🍬 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.

Module elab_config.
  Record record : Set := Build {
    type_logger : option type_logger;
    keep_extra_types_for_interpreter_logging : bool;
    legacy : bool;
  }.
  Definition with_type_logger type_logger (r : record) :=
    Build type_logger r.(keep_extra_types_for_interpreter_logging) r.(legacy).
  Definition with_keep_extra_types_for_interpreter_logging
    keep_extra_types_for_interpreter_logging (r : record) :=
    Build r.(type_logger) keep_extra_types_for_interpreter_logging r.(legacy).
  Definition with_legacy legacy (r : record) :=
    Build r.(type_logger) r.(keep_extra_types_for_interpreter_logging) legacy.
End elab_config.
Definition elab_config := elab_config.record.

[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_starsthstar ⇒ op_starsthstar
    | None ⇒ false
    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 :=
          keep_extra_types_for_interpreter_logging;
        elab_config.legacy := legacy; |}.