(let
'(init_value, reachable) :=
match entrypoints.(Script_typed_ir.entrypoints_node.at_node) with
| Some e =>
((Map.Make Alpha_context.Entrypoint.T).(S.singleton)
e.(Script_typed_ir.entrypoint_info.name) tt, true)
| None => ((Map.Make Alpha_context.Entrypoint.T).(S.empty), false)
end in
let? ' (first_unreachable, all)
:= (fix check
(a : Ty.t) (t_value : With_family.ty a)
(entrypoints0 : Script_typed_ir.entrypoints_node)
(path : list Alpha_context.Script.prim) (reachable0 : bool)
(acc_value : M* list Alpha_context.Script.prim * Entrypoint_repr._Set.(_Set.S.t))
{struct t_value} :
M? (M* list Alpha_context.Script.prim * Entrypoint_repr._Set.(_Set.S.t)) :=
match t_value with
| @With_family.Pair_t t0 t3 _ _ _ _ => return? acc_value
| @With_family.Union_t t0 t3 tl tr _ _ =>
match entrypoints0.(Script_typed_ir.entrypoints_node.nested) with
| Script_typed_ir.Entrypoints_Union e0 =>
let? ' (acc_value0, l_reachable)
:= (let
'(first_unreachable, all) := acc_value in
match
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._left)
.(Script_typed_ir.entrypoints_node.at_node)
with
| Some e =>
if
(Map.Make Alpha_context.Entrypoint.T).(S.mem)
e.(Script_typed_ir.entrypoint_info.name) all
then
Error_monad.error_value
(Build_extensible "Duplicate_entrypoint"
Alpha_context.Entrypoint.t
e.(Script_typed_ir.entrypoint_info.name))
else
return? (first_unreachable,
(Map.Make Alpha_context.Entrypoint.T).(S.add)
e.(Script_typed_ir.entrypoint_info.name) tt all, true)
| None =>
return? (if reachable0
then acc_value
else
match tl with
| @With_family.Pair_t t4 t5 _ _ _ _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
| @With_family.Union_t t4 t5 _ _ _ _ => acc_value
| @With_family.Lambda_t arg ret _ _ _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
| @With_family.Option_t t _ _ _ |
@With_family.List_t t _ _ |
@With_family.Set_t t _ _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
| @With_family.Map_t key value _ _ _ |
@With_family.Big_map_t key value _ _ _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
| @With_family.Contract_t arg _ _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
| @With_family.Ticket_t a0 _ _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
| _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
end, reachable0)
end)
in let? ' (acc_value1, r_reachable)
:= (let
'(first_unreachable, all) := acc_value0 in
match
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._right)
.(Script_typed_ir.entrypoints_node.at_node)
with
| Some e =>
if
(Map.Make Alpha_context.Entrypoint.T).(S.mem)
e.(Script_typed_ir.entrypoint_info.name) all
then
Error_monad.error_value
(Build_extensible "Duplicate_entrypoint"
Alpha_context.Entrypoint.t
e.(Script_typed_ir.entrypoint_info.name))
else
return? (first_unreachable,
(Map.Make Alpha_context.Entrypoint.T).(S.add)
e.(Script_typed_ir.entrypoint_info.name) tt all, true)
| None =>
return? (if reachable0
then acc_value0
else
match tr with
| @With_family.Pair_t t4 t5 _ _ _ _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
| @With_family.Union_t t4 t5 _ _ _ _ => acc_value0
| @With_family.Lambda_t arg ret _ _ _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
| @With_family.Option_t t _ _ _ |
@With_family.List_t t _ _ |
@With_family.Set_t t _ _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
| @With_family.Map_t key value _ _ _ |
@With_family.Big_map_t key value _ _ _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
| @With_family.Contract_t arg _ _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
| @With_family.Ticket_t a0 _ _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
| _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
end, reachable0)
end)
in let? ' acc_value2
:= check t0 tl
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._left)
(Michelson_v1_primitives.D_Left :: path) l_reachable acc_value1
in check t3 tr
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._right)
(Michelson_v1_primitives.D_Right :: path) r_reachable acc_value2
| Script_typed_ir.Entrypoints_None => return? acc_value
end
| @With_family.Lambda_t arg ret _ _ _ => return? acc_value
| @With_family.Option_t t0 _ _ _ | @With_family.List_t t0 _ _ |
@With_family.Set_t t0 _ _ => return? acc_value
| @With_family.Map_t key value _ _ _ | @With_family.Big_map_t key value _ _ _ =>
return? acc_value
| @With_family.Contract_t arg _ _ => return? acc_value
| @With_family.Ticket_t a0 _ _ => return? acc_value
| _ => return? acc_value
end) (Ty.Union t1 t2) full_value entrypoints nil reachable
(None, init_value)
in if
not
((Map.Make Alpha_context.Entrypoint.T).(S.mem) Alpha_context.Entrypoint.default all)
then return_unit
else
match first_unreachable with
| Some path =>
Error_monad.error_value
(Build_extensible "Unreachable_entrypoint" (list Alpha_context.Script.prim)
path)
| None => return_unit
end) =
(let
'(init_value, reachable) :=
match entrypoints.(Script_typed_ir.entrypoints_node.at_node) with
| Some e =>
((Map.Make Alpha_context.Entrypoint.T).(S.singleton)
e.(Script_typed_ir.entrypoint_info.name) tt, true)
| None => ((Map.Make Alpha_context.Entrypoint.T).(S.empty), false)
end in
let? ' (first_unreachable, all)
:= (fix check
(t_value : Script_typed_ir.ty) (entrypoints0 : Script_typed_ir.entrypoints_node)
(path : list Alpha_context.Script.prim) (reachable0 : bool)
(acc_value : M* list Alpha_context.Script.prim * Entrypoint_repr._Set.(_Set.S.t))
{struct t_value} :
M? (M* list Alpha_context.Script.prim * Entrypoint_repr._Set.(_Set.S.t)) :=
match t_value with
| Script_typed_ir.Union_t tl tr _ _ =>
match entrypoints0.(Script_typed_ir.entrypoints_node.nested) with
| Script_typed_ir.Entrypoints_Union e0 =>
let? ' (acc_value0, l_reachable)
:= (let
'(first_unreachable, all) := acc_value in
match
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._left)
.(Script_typed_ir.entrypoints_node.at_node)
with
| Some e =>
if
(Map.Make Alpha_context.Entrypoint.T).(S.mem)
e.(Script_typed_ir.entrypoint_info.name) all
then
Error_monad.error_value
(Build_extensible "Duplicate_entrypoint"
Alpha_context.Entrypoint.t
e.(Script_typed_ir.entrypoint_info.name))
else
return? (first_unreachable,
(Map.Make Alpha_context.Entrypoint.T).(S.add)
e.(Script_typed_ir.entrypoint_info.name) tt all, true)
| None =>
return? (if reachable0
then acc_value
else
match tl with
| Script_typed_ir.Union_t _ _ _ _ => acc_value
| _ =>
match first_unreachable with
| Some _ => acc_value
| None =>
(Some
(rev (Michelson_v1_primitives.D_Left :: path)),
all)
end
end, reachable0)
end)
in let? ' (acc_value1, r_reachable)
:= (let
'(first_unreachable, all) := acc_value0 in
match
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._right)
.(Script_typed_ir.entrypoints_node.at_node)
with
| Some e =>
if
(Map.Make Alpha_context.Entrypoint.T).(S.mem)
e.(Script_typed_ir.entrypoint_info.name) all
then
Error_monad.error_value
(Build_extensible "Duplicate_entrypoint"
Alpha_context.Entrypoint.t
e.(Script_typed_ir.entrypoint_info.name))
else
return? (first_unreachable,
(Map.Make Alpha_context.Entrypoint.T).(S.add)
e.(Script_typed_ir.entrypoint_info.name) tt all, true)
| None =>
return? (if reachable0
then acc_value0
else
match tr with
| Script_typed_ir.Union_t _ _ _ _ => acc_value0
| _ =>
match first_unreachable with
| Some _ => acc_value0
| None =>
(Some
(rev
(Michelson_v1_primitives.D_Right
:: path)), all)
end
end, reachable0)
end)
in let? ' acc_value2
:= check tl
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._left)
(Michelson_v1_primitives.D_Left :: path) l_reachable acc_value1
in check tr
e0
.(Script_typed_ir.ConstructorRecords_nested_entrypoints.nested_entrypoints.Entrypoints_Union._right)
(Michelson_v1_primitives.D_Right :: path) r_reachable acc_value2
| Script_typed_ir.Entrypoints_None => return? acc_value
end
| _ => return? acc_value
end) (With_family.to_ty full_value) entrypoints nil reachable
(None, init_value)
in if
not
((Map.Make Alpha_context.Entrypoint.T).(S.mem) Alpha_context.Entrypoint.default all)
then return_unit
else
match first_unreachable with
| Some path =>
Error_monad.error_value
(Build_extensible "Unreachable_entrypoint" (list Alpha_context.Script.prim)
path)
| None => return_unit
end)
Created
June 21, 2022 15:24
-
-
Save shubhamkumar13/d326459081e7d3a71371034f736f043e to your computer and use it in GitHub Desktop.
subgoal for recursive definition
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment