theory Protocol

imports Codec_Class 

keywords "operation_setup" :: thy_decl % "ML"

begin

ML\<open>

val _ =

  let

    open Protocol

    fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =

      let

        fun eval enclose =

          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)

            (ML_Lex.read ("Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @

              enclose (ML_Lex.read_source false source) @

              ML_Lex.read ")" @

              ML_Lex.read (print_flags flags))

      in

        if auto then

          let

            val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)

            val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)

            val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)

            fun enclose toks =

              ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @

              ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @

              ML_Lex.read "action=" @ toks @ ML_Lex.read "}"

          in

            eval enclose

          end

        else

          eval I

      end

    val parse_flag =

      (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>

        (fn flag => join_flags

           {sequential = flag = "sequential",

            bracket = flag = "bracket",

            auto = flag = "auto"})

    val parse_flags =

      Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)

    val parse_cmd =

      Scan.optional (Args.parens parse_flags) I --

      Parse.name --

      Parse.!!! (@{keyword "="} |-- Parse.ML_source)

  in

    Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"

      (parse_cmd >> (fn ((flags, name), txt) =>

        Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))

  end

\<close>

end