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