Skip to main content

🍬 Script_tc_context.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Definition in_lambda : Set := bool.

Records for the constructor parameters
Module ConstructorRecords_callsite.
  Module callsite.
    Module Toplevel.
      Record record {storage_type param_type entrypoints : Set} : Set := Build {
        storage_type : storage_type;
        param_type : param_type;
        entrypoints : entrypoints;
      }.
      Arguments record : clear implicits.
      Definition with_storage_type {t_storage_type t_param_type t_entrypoints}
        storage_type (r : record t_storage_type t_param_type t_entrypoints) :=
        Build t_storage_type t_param_type t_entrypoints storage_type
          r.(param_type) r.(entrypoints).
      Definition with_param_type {t_storage_type t_param_type t_entrypoints}
        param_type (r : record t_storage_type t_param_type t_entrypoints) :=
        Build t_storage_type t_param_type t_entrypoints r.(storage_type)
          param_type r.(entrypoints).
      Definition with_entrypoints {t_storage_type t_param_type t_entrypoints}
        entrypoints (r : record t_storage_type t_param_type t_entrypoints) :=
        Build t_storage_type t_param_type t_entrypoints r.(storage_type)
          r.(param_type) entrypoints.
    End Toplevel.
    Definition Toplevel_skeleton := Toplevel.record.
  End callsite.
End ConstructorRecords_callsite.
Import ConstructorRecords_callsite.

Reserved Notation "'callsite.Toplevel".

Inductive callsite : Set :=
| Toplevel : 'callsite.Toplevel callsite
| View : callsite
| Data : callsite

where "'callsite.Toplevel" :=
  (callsite.Toplevel_skeleton Script_typed_ir.ty Script_typed_ir.ty
    Script_typed_ir.entrypoints).

Module callsite.
  Include ConstructorRecords_callsite.callsite.
  Definition Toplevel := 'callsite.Toplevel.
End callsite.

Module t.
  Record record : Set := Build {
    callsite : callsite;
    in_lambda : in_lambda;
  }.
  Definition with_callsite callsite (r : record) :=
    Build callsite r.(in_lambda).
  Definition with_in_lambda in_lambda (r : record) :=
    Build r.(callsite) in_lambda.
End t.
Definition t := t.record.

Definition init_value (callsite : callsite) : t :=
  {| t.callsite := callsite; t.in_lambda := false; |}.

Definition toplevel_value
  (storage_type : Script_typed_ir.ty) (param_type : Script_typed_ir.ty)
  (entrypoints : Script_typed_ir.entrypoints) : t :=
  init_value
    (Toplevel
      {| callsite.Toplevel.storage_type := storage_type;
        callsite.Toplevel.param_type := param_type;
        callsite.Toplevel.entrypoints := entrypoints; |}).

Definition view : t := init_value View.

Definition data : t := init_value Data.

Definition add_lambda (tc_context_value : t) : t :=
  t.with_in_lambda true tc_context_value.

Definition is_in_lambda (function_parameter : t) : in_lambda :=
  let '{| t.callsite := _; t.in_lambda := in_lambda |} := function_parameter in
  in_lambda.

Definition check_not_in_view
  (loc_value : Alpha_context.Script.location) (legacy : bool)
  (tc_context_value : t) (prim : Alpha_context.Script.prim) : M? unit :=
  match
    (tc_context_value.(t.callsite),
      match tc_context_value.(t.callsite) with
      | View(is_in_lambda tc_context_value) || legacy
      | _false
      end) with
  | ((Toplevel _ | Data), _)Result.return_unit
  | (View, true)Result.return_unit
  | (View, _)
    Error_monad.error_value
      (Build_extensible "Forbidden_instr_in_context"
        (Alpha_context.Script.location × Script_tc_errors.context_desc ×
          Alpha_context.Script.prim) (loc_value, Script_tc_errors.View, prim))
  end.