Theory ML_Unification.ML_Functor_Instances

✐‹creator "Kevin Kappelmann"›
section ‹ML Functor Instances›
theory ML_Functor_Instances
  imports
    ML_Parsing_Utils
begin

paragraph ‹Summary›
text ‹Utilities for ML functors that create context data.›

ML_file‹functor_instance.ML›
ML_file‹functor_instance_antiquot.ML›

paragraph ‹Example›

ML_command‹
  ―‹some arbitrary functor›
  functor My_Functor(A : sig
    structure FIA : FUNCTOR_INSTANCE_ARGS
    val n : int
  end) =
  struct
    fun get_n () = (Pretty.writeln (Pretty.block
        [Pretty.str "retrieving n from ", Pretty.str A.FIA.full_name]);
      A.n)
  end

  ―‹create an instance (structure) called ‹Test_Functor_Instance››
  @{functor_instance struct_name = Test_Functor_Instance
    and functor_name = My_Functor
    and id = ‹"test"›
    and more_args = ‹val n = 42›}

  val _ = Test_Functor_Instance.get_n ()
›

end