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 FI : FUNCTOR_INSTANCE_BASE
    val n : int
  end) =
  struct
    fun get_n () = (Pretty.writeln (Pretty.block [
        Pretty.str "retrieving n from ", Binding.pretty A.FI.binding,
        Pretty.str " with id ", Pretty.str (quote A.FI.id)
      ]);
      A.n)
  end

  ―‹create an instance (structure) called ‹Test_Functor_Instance››
structure A =
struct
\<^functor_instance>‹struct_name: Test
  functor_name: My_Functor
  path: ‹"A"›
  id: ‹"test"›
  more_args: ‹val n = 42››
end
  val _ = A.Test.get_n ()
›

end