🍬 Script_ir_annot.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.Non_empty_string.
Inductive var_annot : Set :=
| Var_annot : var_annot.
Inductive type_annot : Set :=
| Type_annot : type_annot.
Inductive field_annot : Set :=
| Field_annot : Non_empty_string.t → field_annot.
Definition error_unexpected_annot {A : Set}
(loc_value : Alpha_context.Script.location) (annot : list A) : M? unit :=
match annot with
| [] ⇒ Result.return_unit
| cons _ _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
#[bypass_check(guard)]
Definition string_iter {A : Set}
(p_value : ascii → Pervasives.result unit A) (s_value : string)
(i_value : int) : Pervasives.result unit A :=
let len := String.length s_value in
let fix aux (i_value : int) {struct i_value} : Pervasives.result unit A :=
if i_value ≥i len then
Result.return_unit
else
let? '_ := p_value (String.get s_value i_value) in
aux (i_value +i 1) in
aux i_value.
Definition is_allowed_char (function_parameter : ascii) : bool :=
match function_parameter with
|
("a" % char | "b" % char | "c" % char | "d" % char | "e" % char | "f" % char
| "g" % char | "h" % char | "i" % char | "j" % char | "k" % char |
"l" % char | "m" % char | "n" % char | "o" % char | "p" % char | "q" % char
| "r" % char | "s" % char | "t" % char | "u" % char | "v" % char |
"w" % char | "x" % char | "y" % char | "z" % char | "A" % char | "B" % char
| "C" % char | "D" % char | "E" % char | "F" % char | "G" % char |
"H" % char | "I" % char | "J" % char | "K" % char | "L" % char | "M" % char
| "N" % char | "O" % char | "P" % char | "Q" % char | "R" % char |
"S" % char | "T" % char | "U" % char | "V" % char | "W" % char | "X" % char
| "Y" % char | "Z" % char | "_" % char | "." % char | "%" % char |
"@" % char | "0" % char | "1" % char | "2" % char | "3" % char | "4" % char
| "5" % char | "6" % char | "7" % char | "8" % char | "9" % char) ⇒ true
| _ ⇒ false
end.
Definition check_char
(loc_value : Alpha_context.Script.location) (c_value : ascii) : M? unit :=
if is_allowed_char c_value then
Result.return_unit
else
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value).
Definition max_annot_length : int := 255.
Inductive annot_opt : Set :=
| Field_annot_opt : option Non_empty_string.t → annot_opt
| Type_annot_opt : option type_annot → annot_opt
| Var_annot_opt : option var_annot → annot_opt.
Definition _at : Non_empty_string.t := Non_empty_string.of_string_exn "@".
Definition parse_annot
(loc_value : Alpha_context.Script.location) (s_value : string)
: M? annot_opt :=
let sub_or_wildcard {A : Set}
(wrap : option Non_empty_string.t → A) (s_value : string) : M? A :=
match Non_empty_string.of_string s_value with
| None ⇒ return? (wrap None)
| Some s_value ⇒
match String.get s_value 0 with
|
("a" % char | "b" % char | "c" % char | "d" % char | "e" % char |
"f" % char | "g" % char | "h" % char | "i" % char | "j" % char |
"k" % char | "l" % char | "m" % char | "n" % char | "o" % char |
"p" % char | "q" % char | "r" % char | "s" % char | "t" % char |
"u" % char | "v" % char | "w" % char | "x" % char | "y" % char |
"z" % char | "A" % char | "B" % char | "C" % char | "D" % char |
"E" % char | "F" % char | "G" % char | "H" % char | "I" % char |
"J" % char | "K" % char | "L" % char | "M" % char | "N" % char |
"O" % char | "P" % char | "Q" % char | "R" % char | "S" % char |
"T" % char | "U" % char | "V" % char | "W" % char | "X" % char |
"Y" % char | "Z" % char | "_" % char | "0" % char | "1" % char |
"2" % char | "3" % char | "4" % char | "5" % char | "6" % char |
"7" % char | "8" % char | "9" % char) ⇒
let? '_ := string_iter (check_char loc_value) s_value 1 in
return? (wrap (Some s_value))
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation"
Alpha_context.Script.location loc_value)
end
end in
let len := String.length s_value in
if (len =i 0) || (len >i max_annot_length) then
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
else
let rest := String.sub s_value 1 (len -i 1) in
match String.get s_value 0 with
| ":" % char ⇒
sub_or_wildcard
(fun (a_value : option Non_empty_string.t) ⇒
Type_annot_opt
(Option.map
(fun (function_parameter : Non_empty_string.t) ⇒
let '_ := function_parameter in
Type_annot) a_value)) rest
| "@" % char ⇒
sub_or_wildcard
(fun (a_value : option Non_empty_string.t) ⇒
Var_annot_opt
(Option.map
(fun (function_parameter : Non_empty_string.t) ⇒
let '_ := function_parameter in
Var_annot) a_value)) rest
| "%" % char ⇒
sub_or_wildcard
(fun (a_value : option Non_empty_string.t) ⇒ Field_annot_opt a_value)
rest
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
Definition parse_annots
(loc_value : Alpha_context.Script.location) (op_staroptstar : option bool)
: option bool → list string → M? (list annot_opt) :=
let allow_special_var :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ false
end in
fun (op_staroptstar : option bool) ⇒
let allow_special_field :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ false
end in
fun (l_value : list string) ⇒
List.map_e
(fun (function_parameter : string) ⇒
match
(function_parameter,
match function_parameter with
| "@%" ⇒ allow_special_var
| _ ⇒ false
end,
match function_parameter with
| "@%%" ⇒ allow_special_var
| _ ⇒ false
end,
match function_parameter with
| "%@" ⇒ allow_special_field
| _ ⇒ false
end) with
| ("@%", true, _, _) ⇒ return? (Var_annot_opt (Some Var_annot))
| ("@%%", _, true, _) ⇒ return? (Var_annot_opt (Some Var_annot))
| ("%@", _, _, true) ⇒ return? (Field_annot_opt (Some _at))
| (s_value, _, _, _) ⇒ parse_annot loc_value s_value
end) l_value.
Definition opt_field_of_field_opt
(function_parameter : option Non_empty_string.t) : option field_annot :=
match function_parameter with
| None ⇒ None
| Some a_value ⇒ Some (Field_annot a_value)
end.
Definition classify_annot
(loc_value : Alpha_context.Script.location) (l_value : list annot_opt)
: M?
(list (option var_annot) × list (option type_annot) ×
list (option field_annot)) :=
(* ❌ Use a trivial matching for the `with` clause, like: *)
typ_with_with_non_trivial_matching.
Definition get_one_annot {A : Set}
(loc_value : Alpha_context.Script.location)
(function_parameter : list (option A)) : M? (option A) :=
match function_parameter with
| [] ⇒ Result.return_none
| cons a_value [] ⇒ return? a_value
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
Definition get_two_annot {A : Set}
(loc_value : Alpha_context.Script.location)
(function_parameter : list (option A)) : M? (option A × option A) :=
match function_parameter with
| [] ⇒ return? (None, None)
| cons a_value [] ⇒ return? (a_value, None)
| cons a_value (cons b_value []) ⇒ return? (a_value, b_value)
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
Definition check_type_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value vars in
let? '_ := error_unexpected_annot loc_value fields in
let? _a := get_one_annot loc_value types in
return? tt.
Definition check_composed_type_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value vars in
let? _t := get_one_annot loc_value types in
let? '(_f1, _f2) := get_two_annot loc_value fields in
return? tt.
Definition parse_field_annot
(loc_value : Alpha_context.Script.location) (annot : string)
: M? (option Non_empty_string.t) :=
if
((String.length annot) ≤i 0) ||
(Compare.Char.(Compare.S.op_ltgt) (String.get annot 0) "%" % char)
then
Result.return_none
else
let? function_parameter := parse_annot loc_value annot in
match function_parameter with
| Field_annot_opt annot_opt ⇒ return? annot_opt
| _ ⇒ return? None
end.
Definition is_field_annot
(loc_value : Alpha_context.Script.location) (a_value : string) : M? bool :=
Error_monad.op_gtpipequestion (parse_field_annot loc_value a_value)
Option.is_some.
Definition extract_field_annot (function_parameter : Alpha_context.Script.node)
: M? (Alpha_context.Script.node × option Non_empty_string.t) :=
match function_parameter with
| (Micheline.Prim loc_value prim args annot) as expr ⇒
let fix extract_first
(acc_value : list string) (function_parameter : list string)
: M?
(Micheline.node Alpha_context.Script.location Alpha_context.Script.prim
× option Non_empty_string.t) :=
match function_parameter with
| [] ⇒ return? (expr, None)
| cons s_value rest ⇒
let? function_parameter := parse_field_annot loc_value s_value in
match function_parameter with
| None ⇒ extract_first (cons s_value acc_value) rest
| (Some _) as some_field_annot ⇒
let annot := List.rev_append acc_value rest in
return? ((Micheline.Prim loc_value prim args annot), some_field_annot)
end
end in
extract_first nil annot
| expr ⇒ return? (expr, None)
end.
Definition has_field_annot (node_value : Alpha_context.Script.node) : M? bool :=
let? function_parameter := extract_field_annot node_value in
match function_parameter with
| (_node, Some _) ⇒ return? true
| (_node, None) ⇒ return? false
end.
Definition remove_field_annot (node_value : Alpha_context.Script.node)
: M? Alpha_context.Script.node :=
let? '(node_value, _a) := extract_field_annot node_value in
return? node_value.
Definition extract_entrypoint_annot (node_value : Alpha_context.Script.node)
: M? (Alpha_context.Script.node × option Alpha_context.Entrypoint.t) :=
let? '(node_value, field_annot_opt) := extract_field_annot node_value in
return?
(node_value,
(Option.bind field_annot_opt
(fun (field_annot : Non_empty_string.t) ⇒
Alpha_context.Entrypoint.of_annot_lax_opt field_annot))).
Definition check_var_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? '_ := error_unexpected_annot loc_value fields in
let? _a := get_one_annot loc_value vars in
return? tt.
Definition check_constr_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None (Some true) annot)
(classify_annot loc_value) in
let? _v := get_one_annot loc_value vars in
let? _t := get_one_annot loc_value types in
let? '(_f1, _f2) := get_two_annot loc_value fields in
return? tt.
Definition check_two_var_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? '_ := error_unexpected_annot loc_value fields in
let? '(_a1, _a2) := get_two_annot loc_value vars in
return? tt.
Definition check_destr_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value (Some true) None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? _v := get_one_annot loc_value vars in
let? _f := get_one_annot loc_value fields in
return? tt.
Definition check_unpair_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value (Some true) None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? '(_vcar, _vcdr) := get_two_annot loc_value vars in
let? '(_f1, _f2) := get_two_annot loc_value fields in
return? tt.
Definition parse_entrypoint_annot
(loc_value : Alpha_context.Script.location) (annot : list string)
: M? (option field_annot) :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? f_value := get_one_annot loc_value fields in
let? _v := get_one_annot loc_value vars in
return? f_value.
Definition parse_entrypoint_annot_strict
(loc_value : Alpha_context.Script.location) (annot : list string)
: M? Alpha_context.Entrypoint.t :=
let? function_parameter := parse_entrypoint_annot loc_value annot in
match function_parameter with
| None ⇒ Pervasives.Ok Alpha_context.Entrypoint.default
| Some (Field_annot a_value) ⇒
Alpha_context.Entrypoint.of_annot_strict loc_value a_value
end.
Definition parse_entrypoint_annot_lax
(loc_value : Alpha_context.Script.location) (annot : list string)
: M? Alpha_context.Entrypoint.t :=
let? function_parameter := parse_entrypoint_annot loc_value annot in
match function_parameter with
| None ⇒ Pervasives.Ok Alpha_context.Entrypoint.default
| Some (Field_annot annot) ⇒ Alpha_context.Entrypoint.of_annot_lax annot
end.
Definition check_var_type_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value fields in
let? _v := get_one_annot loc_value vars in
let? _t := get_one_annot loc_value types in
return? tt.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Non_empty_string.
Inductive var_annot : Set :=
| Var_annot : var_annot.
Inductive type_annot : Set :=
| Type_annot : type_annot.
Inductive field_annot : Set :=
| Field_annot : Non_empty_string.t → field_annot.
Definition error_unexpected_annot {A : Set}
(loc_value : Alpha_context.Script.location) (annot : list A) : M? unit :=
match annot with
| [] ⇒ Result.return_unit
| cons _ _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
#[bypass_check(guard)]
Definition string_iter {A : Set}
(p_value : ascii → Pervasives.result unit A) (s_value : string)
(i_value : int) : Pervasives.result unit A :=
let len := String.length s_value in
let fix aux (i_value : int) {struct i_value} : Pervasives.result unit A :=
if i_value ≥i len then
Result.return_unit
else
let? '_ := p_value (String.get s_value i_value) in
aux (i_value +i 1) in
aux i_value.
Definition is_allowed_char (function_parameter : ascii) : bool :=
match function_parameter with
|
("a" % char | "b" % char | "c" % char | "d" % char | "e" % char | "f" % char
| "g" % char | "h" % char | "i" % char | "j" % char | "k" % char |
"l" % char | "m" % char | "n" % char | "o" % char | "p" % char | "q" % char
| "r" % char | "s" % char | "t" % char | "u" % char | "v" % char |
"w" % char | "x" % char | "y" % char | "z" % char | "A" % char | "B" % char
| "C" % char | "D" % char | "E" % char | "F" % char | "G" % char |
"H" % char | "I" % char | "J" % char | "K" % char | "L" % char | "M" % char
| "N" % char | "O" % char | "P" % char | "Q" % char | "R" % char |
"S" % char | "T" % char | "U" % char | "V" % char | "W" % char | "X" % char
| "Y" % char | "Z" % char | "_" % char | "." % char | "%" % char |
"@" % char | "0" % char | "1" % char | "2" % char | "3" % char | "4" % char
| "5" % char | "6" % char | "7" % char | "8" % char | "9" % char) ⇒ true
| _ ⇒ false
end.
Definition check_char
(loc_value : Alpha_context.Script.location) (c_value : ascii) : M? unit :=
if is_allowed_char c_value then
Result.return_unit
else
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value).
Definition max_annot_length : int := 255.
Inductive annot_opt : Set :=
| Field_annot_opt : option Non_empty_string.t → annot_opt
| Type_annot_opt : option type_annot → annot_opt
| Var_annot_opt : option var_annot → annot_opt.
Definition _at : Non_empty_string.t := Non_empty_string.of_string_exn "@".
Definition parse_annot
(loc_value : Alpha_context.Script.location) (s_value : string)
: M? annot_opt :=
let sub_or_wildcard {A : Set}
(wrap : option Non_empty_string.t → A) (s_value : string) : M? A :=
match Non_empty_string.of_string s_value with
| None ⇒ return? (wrap None)
| Some s_value ⇒
match String.get s_value 0 with
|
("a" % char | "b" % char | "c" % char | "d" % char | "e" % char |
"f" % char | "g" % char | "h" % char | "i" % char | "j" % char |
"k" % char | "l" % char | "m" % char | "n" % char | "o" % char |
"p" % char | "q" % char | "r" % char | "s" % char | "t" % char |
"u" % char | "v" % char | "w" % char | "x" % char | "y" % char |
"z" % char | "A" % char | "B" % char | "C" % char | "D" % char |
"E" % char | "F" % char | "G" % char | "H" % char | "I" % char |
"J" % char | "K" % char | "L" % char | "M" % char | "N" % char |
"O" % char | "P" % char | "Q" % char | "R" % char | "S" % char |
"T" % char | "U" % char | "V" % char | "W" % char | "X" % char |
"Y" % char | "Z" % char | "_" % char | "0" % char | "1" % char |
"2" % char | "3" % char | "4" % char | "5" % char | "6" % char |
"7" % char | "8" % char | "9" % char) ⇒
let? '_ := string_iter (check_char loc_value) s_value 1 in
return? (wrap (Some s_value))
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation"
Alpha_context.Script.location loc_value)
end
end in
let len := String.length s_value in
if (len =i 0) || (len >i max_annot_length) then
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
else
let rest := String.sub s_value 1 (len -i 1) in
match String.get s_value 0 with
| ":" % char ⇒
sub_or_wildcard
(fun (a_value : option Non_empty_string.t) ⇒
Type_annot_opt
(Option.map
(fun (function_parameter : Non_empty_string.t) ⇒
let '_ := function_parameter in
Type_annot) a_value)) rest
| "@" % char ⇒
sub_or_wildcard
(fun (a_value : option Non_empty_string.t) ⇒
Var_annot_opt
(Option.map
(fun (function_parameter : Non_empty_string.t) ⇒
let '_ := function_parameter in
Var_annot) a_value)) rest
| "%" % char ⇒
sub_or_wildcard
(fun (a_value : option Non_empty_string.t) ⇒ Field_annot_opt a_value)
rest
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
Definition parse_annots
(loc_value : Alpha_context.Script.location) (op_staroptstar : option bool)
: option bool → list string → M? (list annot_opt) :=
let allow_special_var :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ false
end in
fun (op_staroptstar : option bool) ⇒
let allow_special_field :=
match op_staroptstar with
| Some op_starsthstar ⇒ op_starsthstar
| None ⇒ false
end in
fun (l_value : list string) ⇒
List.map_e
(fun (function_parameter : string) ⇒
match
(function_parameter,
match function_parameter with
| "@%" ⇒ allow_special_var
| _ ⇒ false
end,
match function_parameter with
| "@%%" ⇒ allow_special_var
| _ ⇒ false
end,
match function_parameter with
| "%@" ⇒ allow_special_field
| _ ⇒ false
end) with
| ("@%", true, _, _) ⇒ return? (Var_annot_opt (Some Var_annot))
| ("@%%", _, true, _) ⇒ return? (Var_annot_opt (Some Var_annot))
| ("%@", _, _, true) ⇒ return? (Field_annot_opt (Some _at))
| (s_value, _, _, _) ⇒ parse_annot loc_value s_value
end) l_value.
Definition opt_field_of_field_opt
(function_parameter : option Non_empty_string.t) : option field_annot :=
match function_parameter with
| None ⇒ None
| Some a_value ⇒ Some (Field_annot a_value)
end.
Definition classify_annot
(loc_value : Alpha_context.Script.location) (l_value : list annot_opt)
: M?
(list (option var_annot) × list (option type_annot) ×
list (option field_annot)) :=
(* ❌ Use a trivial matching for the `with` clause, like: *)
typ_with_with_non_trivial_matching.
Definition get_one_annot {A : Set}
(loc_value : Alpha_context.Script.location)
(function_parameter : list (option A)) : M? (option A) :=
match function_parameter with
| [] ⇒ Result.return_none
| cons a_value [] ⇒ return? a_value
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
Definition get_two_annot {A : Set}
(loc_value : Alpha_context.Script.location)
(function_parameter : list (option A)) : M? (option A × option A) :=
match function_parameter with
| [] ⇒ return? (None, None)
| cons a_value [] ⇒ return? (a_value, None)
| cons a_value (cons b_value []) ⇒ return? (a_value, b_value)
| _ ⇒
Error_monad.error_value
(Build_extensible "Unexpected_annotation" Alpha_context.Script.location
loc_value)
end.
Definition check_type_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value vars in
let? '_ := error_unexpected_annot loc_value fields in
let? _a := get_one_annot loc_value types in
return? tt.
Definition check_composed_type_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value vars in
let? _t := get_one_annot loc_value types in
let? '(_f1, _f2) := get_two_annot loc_value fields in
return? tt.
Definition parse_field_annot
(loc_value : Alpha_context.Script.location) (annot : string)
: M? (option Non_empty_string.t) :=
if
((String.length annot) ≤i 0) ||
(Compare.Char.(Compare.S.op_ltgt) (String.get annot 0) "%" % char)
then
Result.return_none
else
let? function_parameter := parse_annot loc_value annot in
match function_parameter with
| Field_annot_opt annot_opt ⇒ return? annot_opt
| _ ⇒ return? None
end.
Definition is_field_annot
(loc_value : Alpha_context.Script.location) (a_value : string) : M? bool :=
Error_monad.op_gtpipequestion (parse_field_annot loc_value a_value)
Option.is_some.
Definition extract_field_annot (function_parameter : Alpha_context.Script.node)
: M? (Alpha_context.Script.node × option Non_empty_string.t) :=
match function_parameter with
| (Micheline.Prim loc_value prim args annot) as expr ⇒
let fix extract_first
(acc_value : list string) (function_parameter : list string)
: M?
(Micheline.node Alpha_context.Script.location Alpha_context.Script.prim
× option Non_empty_string.t) :=
match function_parameter with
| [] ⇒ return? (expr, None)
| cons s_value rest ⇒
let? function_parameter := parse_field_annot loc_value s_value in
match function_parameter with
| None ⇒ extract_first (cons s_value acc_value) rest
| (Some _) as some_field_annot ⇒
let annot := List.rev_append acc_value rest in
return? ((Micheline.Prim loc_value prim args annot), some_field_annot)
end
end in
extract_first nil annot
| expr ⇒ return? (expr, None)
end.
Definition has_field_annot (node_value : Alpha_context.Script.node) : M? bool :=
let? function_parameter := extract_field_annot node_value in
match function_parameter with
| (_node, Some _) ⇒ return? true
| (_node, None) ⇒ return? false
end.
Definition remove_field_annot (node_value : Alpha_context.Script.node)
: M? Alpha_context.Script.node :=
let? '(node_value, _a) := extract_field_annot node_value in
return? node_value.
Definition extract_entrypoint_annot (node_value : Alpha_context.Script.node)
: M? (Alpha_context.Script.node × option Alpha_context.Entrypoint.t) :=
let? '(node_value, field_annot_opt) := extract_field_annot node_value in
return?
(node_value,
(Option.bind field_annot_opt
(fun (field_annot : Non_empty_string.t) ⇒
Alpha_context.Entrypoint.of_annot_lax_opt field_annot))).
Definition check_var_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? '_ := error_unexpected_annot loc_value fields in
let? _a := get_one_annot loc_value vars in
return? tt.
Definition check_constr_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None (Some true) annot)
(classify_annot loc_value) in
let? _v := get_one_annot loc_value vars in
let? _t := get_one_annot loc_value types in
let? '(_f1, _f2) := get_two_annot loc_value fields in
return? tt.
Definition check_two_var_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? '_ := error_unexpected_annot loc_value fields in
let? '(_a1, _a2) := get_two_annot loc_value vars in
return? tt.
Definition check_destr_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value (Some true) None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? _v := get_one_annot loc_value vars in
let? _f := get_one_annot loc_value fields in
return? tt.
Definition check_unpair_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value (Some true) None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? '(_vcar, _vcdr) := get_two_annot loc_value vars in
let? '(_f1, _f2) := get_two_annot loc_value fields in
return? tt.
Definition parse_entrypoint_annot
(loc_value : Alpha_context.Script.location) (annot : list string)
: M? (option field_annot) :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value types in
let? f_value := get_one_annot loc_value fields in
let? _v := get_one_annot loc_value vars in
return? f_value.
Definition parse_entrypoint_annot_strict
(loc_value : Alpha_context.Script.location) (annot : list string)
: M? Alpha_context.Entrypoint.t :=
let? function_parameter := parse_entrypoint_annot loc_value annot in
match function_parameter with
| None ⇒ Pervasives.Ok Alpha_context.Entrypoint.default
| Some (Field_annot a_value) ⇒
Alpha_context.Entrypoint.of_annot_strict loc_value a_value
end.
Definition parse_entrypoint_annot_lax
(loc_value : Alpha_context.Script.location) (annot : list string)
: M? Alpha_context.Entrypoint.t :=
let? function_parameter := parse_entrypoint_annot loc_value annot in
match function_parameter with
| None ⇒ Pervasives.Ok Alpha_context.Entrypoint.default
| Some (Field_annot annot) ⇒ Alpha_context.Entrypoint.of_annot_lax annot
end.
Definition check_var_type_annot
(loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
let? '(vars, types, fields) :=
Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
(classify_annot loc_value) in
let? '_ := error_unexpected_annot loc_value fields in
let? _v := get_one_annot loc_value vars in
let? _t := get_one_annot loc_value types in
return? tt.