Theory Automatic_Refinement.Prio_List

```section ‹Priority Lists›
theory Prio_List
imports Main
begin
ML ‹
(*
We provide a list of items with insertion operation relative to other
items (after, before) and relative to absolute positions (first, last).
*)
signature PRIO_LIST = sig
type T
type item

val empty: T
val add_first: T -> item -> T
val add_last: T -> item -> T
val add_before: T -> item -> item -> T
val add_after: T -> item -> item -> T

val delete: item -> T -> T

val prio_of: (item -> bool) -> (item * item -> bool) -> T -> int
val contains: T -> item -> bool

val dest: T -> item list

val merge: T * T -> T  (* Ignore conflicts *)
val merge': T * T -> item list * T (* Return conflicting items *)

end

functor Prio_List (
type item;
val eq: item * item -> bool
): PRIO_LIST = struct
type item = item
type T = item list

val empty = []
fun add_first l e = remove eq e l@[e]
fun add_last l e = e::remove eq e l

fun add_before l e a = let
val l = remove eq e l
val (l1,(l2,l3)) = chop_prefix (fn x => not (eq (x,a))) l ||> chop 1
in l1@l2@e::l3 end;

fun add_after l e b = let
val l = remove eq e l
val (l1,l2) = chop_prefix (fn x => not (eq (x,b))) l
in l1@e::l2 end

val delete = remove eq

fun prio_of P prefer l = let
fun do_prefer _ NONE = true
| do_prefer x (SOME (_,y)) = prefer (x,y)

fun pr [] _ st = (case st of NONE => ~1 | SOME (i,_) => i)
| pr (x::l) i st = if P x andalso do_prefer x st then
pr l (i+1) (SOME (i,x))
else
pr l (i+1) st

in
pr l 0 NONE
end

val contains = member eq

fun dest l = l

fun merge' (l1,l2) = let
val l1' = map (fn ty => (Library.member eq l2 ty,ty)) l1;
val l2' = map (fn ty => (Library.member eq l1 ty,ty)) l2;

fun m []                []               = []
| m []                l                = map (apfst (K false)) l
| m l                 []               = map (apfst (K false)) l
| m ((true,t1)::l1)   ((true,t2)::l2)  =
(not (eq (t1,t2)),t2) :: m l1 l2
| m ((false,t1)::l1)  ((true,t2)::l2)  =
(false,t1) :: m l1 ((true,t2)::l2)
| m ((true,t1)::l1)   ((false,t2)::l2) =
(false,t2) :: m ((true,t1)::l1) l2
| m ((false,t1)::l1)  ((false,t2)::l2) =
(false,t2)::(false,t1)::m l1 l2

val r = m l1' l2'
in
(map #2 (filter #1 r), map #2 r)
end;

fun merge (l1,l2) = #2 (merge' (l1,l2))

end
›

end
```