Skip to main content

🍬 Script_ir_translator_config.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require TezosOfOCaml.Proto_alpha.Alpha_context.

[type_logger] is a function, whose task is to log how a stack's type is altered by some operation being logged.
Definition type_logger : Set :=
  Alpha_context.Script.location list Alpha_context.Script.expr
  list Alpha_context.Script.expr unit.

[elab_config] is a record grouping together some flags and options shared by many of the functions in [Script_ir_translator]. It's convenient to group them together, because they're of similar types ([bool] or ['a option]), so they're easier not to mix together. It also makes for shorter and more readable function calls.
[make ?type_logger ?logging_enabled ~legacy ()] creates an [elab_config] record to be passed to parsing functions in [Script_ir_translator].
Note: [?logging_enabled] defaults to [false], because it only ever should be set to [true] if the Translator is called from outside the protocol (i.e. from the Plugin).
Definition make
  (type_logger_value : option type_logger) (op_staroptstar : option bool)
  : bool unit elab_config :=
  let keep_extra_types_for_interpreter_logging :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | Nonefalse
    end in
  fun (legacy : bool) ⇒
    fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      {| elab_config.type_logger := type_logger_value;
        elab_config.keep_extra_types_for_interpreter_logging :=
        elab_config.legacy := legacy; |}.