Theory SAIS

theory SAIS
  imports Induce Get_Types
begin

section "SAIS"

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

      ―‹ Compute the suffix types ›
      ST = abs_get_suffix_types T;

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

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

      ―‹ Extract the LMS types ›
      LMS1 = extract_lms ST SA;

      ―‹ Create a new alphabet ›
      names = rename_mapping T ST LMS1;

      ―‹ Make a reduced string (2 lines) ›
      T' = rename_string LMS0 names;

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

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

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

      ―‹ Compute the suffix types ›
      ST = get_suffix_types T;

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

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

      ―‹ Extract the LMS types ›
      LMS1 = extract_lms ST SA;

      ―‹ Create a new alphabet ›
      names = rename_mapping T ST LMS1;

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

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

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

abbreviation "sais ≡ sais_r1"

end