-
Notifications
You must be signed in to change notification settings - Fork 0
/
ccgen_util.v
21 lines (18 loc) · 726 Bytes
/
ccgen_util.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
From mathcomp Require Import all_ssreflect.
From Michocoq Require Import semantics util macros.
Import syntax comparable error.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import String.
Open Scope string_scope.
Definition make_typed_validation_snippet genparam_ty
(typed_validation_snippet :
instruction_seq None false (genparam_ty ::: mutez ::: [::]) [::])
: instruction_seq None false (pair bytes mutez ::: [::])
(pair bytes mutez ::: [::]) :=
{
DUP; DIP1 {UNPAIR; UNPACK genparam_ty};
DIP1 {IF_NONE {PUSH _ (Comparable_constant syntax_type.string "genparam is of wrong type"); FAILWITH}
typed_validation_snippet}
}.