Theory ML_Unification.ML_Parsing_Utils

✐‹creator "Kevin Kappelmann"›
section ‹ML Parsing Utils›
theory ML_Parsing_Utils
  imports
    ML_Attributes
    ML_Attribute_Utils
begin

paragraph ‹Summary›
text ‹Parsing utilities for ML. We provide an antiquotation that takes a list of
keys and creates a corresponding record with getters and mappers and a parser for corresponding
key-value pairs.›

ML_file‹parse_util.ML›

ML_file‹parse_key_value.ML›
ML_file‹parse_key_value_antiquot.ML›

(*use the following to test the code generation*)
(* ML_command‹
  Parse_Key_Value_Antiquot.mk_all "Test" NONE ["ABC", "DEFG" ]
  |> split_lines |> map Pretty.str |> Pretty.fbreaks |> Pretty.block |> Pretty.writeln
› *)

paragraph ‹Example›

ML_command‹
  ― ‹Create record type and utility functions.›
  @{parse_entries (struct) Test [ABC, DEFG]}

  val parser =
    let
      ― ‹Create the key-value parser.›
      val parse_entry = Parse_Key_Value.parse_entry
        Test.parse_key ―‹parser for keys›
        (Scan.succeed [])  ―‹delimiter parser›
        (Test.parse_entry ―‹value parser›
          Parse.string ―‹parser for ABC›
          Parse.int) ―‹parser for DEFG›
      val required_keys = [Test.key Test.ABC] ―‹required keys›
      val default_entries = Test.empty_entries () ―‹default values for entries›
    in Test.parse_entries_required Parse.and_list1 required_keys parse_entry default_entries end
    ― ‹This parses, for example, ‹ABC = hello and DEFG = 3› or ‹DEFG = 3 and ABC = hello›,
    but not ‹DEFG = 3› since the key "ABC" is missing.›
›

end