🍬 Script_tc_context.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
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.