Theory BasicAlgorithms

subsection ‹Basic Algorithms›

theory BasicAlgorithms
  imports Data ErrorMonad
begin

text ‹
  In this section, we introduce preliminary definitions and functions, required by the
  integration and edit algorithms in the following sections.
›

definition ext_ids :: "('ℐ, 'Σ) woot_character list ⇒ 'ℐ extended list"
  where "ext_ids s = ⊢#(map (λx. ⟦ I x ⟧) s)@[⊣]"

text ‹
  The function @{term ext_ids} returns the set of extended identifiers in a string @{term s},
  including the beginning and end markers @{term "⊢"} and @{term "⊣"}.
›

fun idx :: "('ℐ, 'Σ) woot_character list ⇒ 'ℐ extended ⇒ error + nat"
  where
    "idx s i = fromSingleton (filter (λj. (ext_ids s ! j = i)) [0..<(length (ext_ids s))])"

text ‹
  The function @{term idx} returns the index in @{term w} of a W-character with a given identifier
   @{term i}:
  %
  \begin{itemize}
  \item If the identifier @{term i} occurs exactly once in the string then
        @{term "idx s ⟦i⟧ = return (j+1)"} where @{term "I (s ! j) = i"}, otherwise
        @{term "idx s ⟦i⟧"} will be an error.
  \item @{term "idx s ⊢ = Inr 0"} and @{term "idx s ⊣ = return (length w + 1)"}.
  \end{itemize}
›

fun nth :: "('ℐ, 'Σ) woot_character list ⇒ nat ⇒ error + ('ℐ, 'Σ) woot_character"
  where
    "nth s 0 = error (STR ''Index has to be >= 1.'')" |
    "nth s (Suc k) = (
      if k < (length s) then
        return (s ! k)
      else
        error (STR ''Index has to be <= length s''))"

text ‹
  The function @{text nth} returns the W-character at a given index in @{term s}.
  The first character has the index 1.
›

fun list_update ::
  "('ℐ, 'Σ) woot_character list ⇒ nat ⇒ ('ℐ, 'Σ) woot_character ⇒ 
  error + ('ℐ, 'Σ) woot_character list"
  where
    "list_update s (Suc k) v = (
        if k < length s then
          return (List.list_update s k v)
        else
          error (STR ''Illegal arguments.''))" |
    "list_update _ 0 _ = error (STR ''Illegal arguments.'')"

text ‹
  The function @{text list_update} substitutes the W-character at the index @{term "k"} in
  @{term s} with the W-character @{term v}. As before, we use the convention of using the index 1
  for the first character.
›

end