Theory Abs_SAIS

theory Abs_SAIS
  imports "../prop/Buckets"
          "../prop/LMS_List_Slice_Util"
          "../../util/Repeat"
begin 

section ‹Induce Sorting›

subsection ‹Bucket Insert›

fun abs_bucket_insert ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list ⇒
   nat list ⇒
   nat list"
  where
"abs_bucket_insert α T _ SA [] = SA" |
"abs_bucket_insert α T B SA (x # xs) =
  (let b = α (T ! x);
       k = B ! b - Suc 0;
       SA' = SA[k := x];
       B' = B[b := k]
   in abs_bucket_insert α T B' SA' xs)"

subsection ‹Induce L-types›

fun abs_induce_l_step ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list ⇒
   nat list × nat list × nat"
  where
"abs_induce_l_step (B, SA, i) (α, T) =
  (if i < length SA ∧ SA ! i < length T
   then
     (case SA ! i of
        Suc j ⇒
          (case suffix_type T j of
             L_type ⇒
               (let k = α (T ! j);
                    l = B ! k
                in (B[k := Suc l], SA[l := j], Suc i))
             | _ ⇒ (B, SA, Suc i))
        | _ ⇒ (B, SA, Suc i))
   else (B, SA, Suc i))"

definition abs_induce_l_base ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list ⇒
   nat list × nat list × nat"
  where
"abs_induce_l_base α T B SA = repeat (length T) abs_induce_l_step (B, SA, 0) (α, T)"

definition abs_induce_l ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list ⇒
   nat list"
  where
"abs_induce_l α T B SA =
  (let (B', SA', i) = abs_induce_l_base α T B SA
   in SA')"

subsection ‹Induce S-types›

fun abs_induce_s_step ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list ⇒
   nat list × nat list × nat"
  where
"abs_induce_s_step (B, SA, i) (α, T) =
  (case i of
    Suc n ⇒
      (if Suc n < length SA ∧ SA ! Suc n < length T then
        (case SA ! Suc n of
          Suc j ⇒
            (case suffix_type T j of
              S_type ⇒
                (let b = α (T ! j);
                     k = B ! b - Suc 0
                 in (B[b := k], SA[k := j], n)
                )
              | _ ⇒ (B, SA, n)
            )
          | _ ⇒ (B, SA, n)
        )
        else
          (B, SA, n)
       )
    | _   ⇒ (B, SA, 0)
  )"

definition abs_induce_s_base ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list ⇒
   nat list × nat list × nat"
  where
"abs_induce_s_base α T B SA = repeat (length T) abs_induce_s_step (B, SA, length T) (α, T)"

definition abs_induce_s ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list ⇒
   nat list"
  where
"abs_induce_s α T B SA =
  (let (B', SA', i) = abs_induce_s_base α T B SA
   in SA')"

subsection ‹Induce Sorting›

definition abs_sa_induce ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list"
  where
"abs_sa_induce α T LMS =
  (let
      B0 = map (bucket_end α T) [0..<Suc (α (Max (set T)))];
      B1 = map (bucket_start α T) [0..<Suc (α (Max (set T)))];

      ―‹Initialise SA›
      SA = replicate (length T) (length T);

      ―‹Insert the LMS types into the suffix array ›
      SA = abs_bucket_insert α T B0 SA (rev LMS);

      ―‹Insert the L types into the suffix array ›
      SA = abs_induce_l α T B1 SA

   ―‹Insert the S types into the suffix array ›
   in abs_induce_s α T (B0[0 := 0]) SA)"

section ‹Rename Mapping›

fun abs_rename_mapping' ::
  "('a :: {linorder, order_bot}) list ⇒
    nat list ⇒
    nat list ⇒
    nat ⇒
    nat list"
  where
"abs_rename_mapping' _ [] names _  = names" |
"abs_rename_mapping' _ [x] names i = names[x := i]" |
"abs_rename_mapping' T (a # b # xs) names i =
  (if lms_slice T a = lms_slice T b
    then abs_rename_mapping' T (b # xs) (names[a := i]) i
   else abs_rename_mapping' T (b # xs) (names[a := i]) (Suc i))"

definition abs_rename_mapping :: "('a :: {linorder, order_bot}) list ⇒ nat list ⇒ nat list"
  where
"abs_rename_mapping T LMS = abs_rename_mapping' T LMS (replicate (length T) (length T)) 0"


section ‹Rename String›

fun rename_string :: "nat list ⇒ nat list ⇒ nat list"
  where
"rename_string [] _ = []" |
"rename_string (x#xs) names = (names ! x) # rename_string xs names"

section ‹Order LMS›

fun order_lms :: "nat list ⇒ nat list ⇒ nat list"
  where
"order_lms LMS [] = []" |
"order_lms LMS (x # xs) = LMS ! x # order_lms LMS xs"

section ‹Extract LMS›

abbreviation abs_extract_lms :: "('a :: {linorder, order_bot}) list ⇒ nat list ⇒ nat list"
  where
"abs_extract_lms ≡ filter ∘ abs_is_lms "

section ‹SAIS Definition›

function abs_sais ::
  "nat list ⇒
   nat list"
where
  "abs_sais [] = []" |
  "abs_sais [x] = [0]" |
  "abs_sais (a # b # xs) =
   (let
      T = a # b # xs;

      ―‹ Extract the LMS types ›
      LMS0 = abs_extract_lms T [0..<length T];

      ―‹ Induce the prefix ordering based on LMS ›
      SA = abs_sa_induce id T LMS0;

      ―‹ Extract the LMS types ›
      LMS = abs_extract_lms T SA;

      ―‹ Create a new alphabet ›
      names = abs_rename_mapping T LMS;

      ―‹ Make a reduced string ›
      T' = rename_string LMS0 names;

      ―‹ Obtain the correct ordering of LMS-types ›
      LMS = (if distinct T' then LMS else order_lms LMS0 (abs_sais T'))

   ―‹ Induce the suffix ordering based of LMS ›
   in abs_sa_induce id T LMS)"
  by pat_completeness blast+

end