Theory Induce

theory Induce
  imports Induce_S Induce_L Bucket_Insert 
begin

section "Induce"

definition sa_induce_r0 ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   nat list ⇒
   nat list"
  where
"sa_induce_r0 α 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);

      ―‹Get the suffix types›
      ST = abs_get_suffix_types 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 = induce_l α T ST B1 SA

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

definition sa_induce_r1 ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   SL_types list ⇒
   nat list ⇒
   nat list"
  where
"sa_induce_r1 α T ST 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 = induce_l α T ST B1 SA

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

definition sa_induce_r2 ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   SL_types list ⇒
   nat list ⇒
   nat list"
  where
"sa_induce_r2 α T ST 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 = bucket_insert α T B0 SA (rev LMS);

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

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

abbreviation "sa_induce ≡ sa_induce_r2"

end