Theory Byte_Level_Encoding.Focus_Parser

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Focus_Parser
  imports Lenses_And_Other_Optics.Focus Lenses_And_Other_Optics.List_Optics Lenses_And_Other_Optics.Array_Optics
begin
(*>*)

section‹Focus parsers›

subsection‹Definition›

datatype ('a, 'r) focus_parser
  = FocusParser (run_parser: ‹('a, 'r × 'a) focus›)

subsection‹Parser combinators›

text‹Parsers can be sequenced:›

lift_definition iso_focus_prod_assoc :: ‹('a × 'b × 'c, ('a × 'b) × 'c) focus› is
  ‹iso⇩∫ (λ(x,y,z). ((x,y),z)) (λ((x,y),z). (x,y,z))›
by (simp add: case_prod_beta iso_focus_raw_valid)

text‹Use eta expansion during code generation to avoid ML value restriction:›
definition iso_focus_prod_assoc_lazy :: ‹unit ⇒ ('a × 'b × 'c, ('a × 'b) × 'c) focus› where
  ‹iso_focus_prod_assoc_lazy _ = iso_focus_prod_assoc›

declare iso_focus_prod_assoc_lazy_def [of ‹()›, symmetric, code_unfold]
declare iso_focus_prod_assoc_lazy_def [THEN  arg_cong[where f="Rep_focus"], simplified iso_focus_prod_assoc.rep_eq, code]

lemma iso_focus_prod_components[focus_components]:
  shows ‹focus_view iso_focus_prod_assoc (x,y,z) = Some ((x,y),z)›
    and ‹focus_update iso_focus_prod_assoc ((x,y),z) t = (x,y,z)› 
by (transfer; clarsimp simp add: iso_focus_raw_components)+

definition focus_parser_sequence :: ‹('a, 'r) focus_parser ⇒ ('a, 's) focus_parser ⇒
     ('a, 'r × 's) focus_parser› (infixl "--⇩∫" 58) where
  ‹focus_parser_sequence p0 p1 ≡ FocusParser (run_parser p0 ⋄ (id⇩∫ ×⇩∫ run_parser p1) ⋄ iso_focus_prod_assoc)›

text‹Parsers can be refined by applying a focus to a parsing result:›
definition focus_parser_map :: ‹('a, 'r) focus_parser ⇒ ('r, 's) focus ⇒
      ('a, 's) focus_parser› (infixl ">>⇩∫" 61) where
  ‹focus_parser_map p0 f ≡ FocusParser (run_parser p0 ⋄ (f ×⇩∫ id⇩∫))›

text‹With sequencing and forgetting, we can build a sequence combinator for parsers which forgets
the result of one of the two parsers:›
abbreviation focus_parser_sequence_forgetL :: ‹('a, 'r) focus_parser ⇒ ('a, 's) focus_parser ⇒
      ('a, 's) focus_parser› (infixl "|--⇩∫" 58) where
  ‹focus_parser_sequence_forgetL p0 p1 ≡ (p0 --⇩∫ p1) >>⇩∫ snd⇩∫›

abbreviation focus_parser_sequence_forgetR :: ‹('a, 'r) focus_parser ⇒ ('a, 's) focus_parser ⇒
      ('a, 'r) focus_parser› (infixl "--|⇩∫" 58) where
  ‹focus_parser_sequence_forgetR p0 p1 ≡ (p0 --⇩∫ p1) >>⇩∫ fst⇩∫›

bundle code_parser_notation
begin
  notation focus_parser_sequence (infixl "--" 58)
  notation focus_parser_map (infixl ">>" 61)
  notation focus_parser_sequence_forgetR (infixl "--|" 58) 
  notation focus_parser_sequence_forgetL (infixl "|--" 58) 
end

subsection‹Closing a parser›

text‹After parsing, we can forget the remaining data to obtain a focus onto the target value type:›
definition run_parser_partial :: ‹('a, 'r) focus_parser ⇒ ('a, 'r) focus› where
  ‹run_parser_partial p ≡ run_parser p ⋄ fst⇩∫›

text‹We may also want to check that we have consumed all data before closing the parser:›
definition run_parser_all :: ‹('a list, 'r) focus_parser ⇒ ('a list, 'r) focus› where
  ‹run_parser_all p ≡ run_parser p ⋄ (id⇩∫ ×⇩∫ list_empty_focus) ⋄ fst⇩∫›

subsection‹Basic parsers›

text‹Parse a single element from a list:›
definition parse_single :: ‹('a list, 'a) focus_parser› where
  [code_unfold]: ‹parse_single ≡ FocusParser list_nonempty_focus›

text‹Parse a fixed number of elements off a list, into an array:›
definition parse_array :: ‹('a list, ('a, 'l::{len}) array) focus_parser› where
  ‹parse_array ≡ FocusParser list_minlen_focus›

abbreviation parse_array2 :: ‹('a list, ('a, 2) array) focus_parser› where
  ‹parse_array2 ≡ parse_array›
abbreviation parse_array4 :: ‹('a list, ('a, 4) array) focus_parser› where
  ‹parse_array4 ≡ parse_array›
abbreviation parse_array8 :: ‹('a list, ('a, 8) array) focus_parser› where
  ‹parse_array8 ≡ parse_array›

(*<*)
end
(*>*)