val serialize32_maybe_enum_key_tac:
    #k: parser_kind ->
    #key: eqtype ->
    #repr: eqtype ->
    #p: parser k repr ->
    #s: serializer p ->
    s32: serializer32 s ->
    e: enum key repr {Cons? e} ->
    Prims.unit
  -> T.Tac unit
let serialize32_maybe_enum_key_tac
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (#s: serializer p)
  (s32: serializer32 s)
  (e: enum key repr { Cons? e } )
  ()
: T.Tac unit
= let fu = quote (serialize32_maybe_enum_key_gen #k #key #repr #p #s s32 e) in
  apply fu;
  T.iseq [
    T.solve_vc;
    T.solve_vc;
    T.solve_vc;
    T.solve_vc;
    (fun () -> enum_repr_of_key_tac e);
  ]
val serialize32_maybe_enum_key_tac:
    #k: parser_kind ->
    #key: eqtype ->
    #repr: eqtype ->
    #p: parser k repr ->
    #s: serializer p ->
    s32: serializer32 s ->
    e: enum key repr {Cons? e} ->
    Prims.unit
  -> T.Tac unit
let serialize32_maybe_enum_key_tac
      (#k: parser_kind)
      (#key: eqtype)
      (#repr: eqtype)
      (#p: parser k repr)
      (#s: serializer p)
      (s32: serializer32 s)
      (e: enum key repr {Cons? e})
      ()
    : T.Tac unit =
let fu = quote (serialize32_maybe_enum_key_gen #k #key #repr #p #s s32 e) in
apply fu;
T.iseq [T.solve_vc; T.solve_vc; T.solve_vc; T.solve_vc; (fun () -> enum_repr_of_key_tac e)]
LowParse.SLow.Tac.Enum.fst.checked
prims.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.Tac.Enum.fst.checked LowParse.SLow.Enum.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.Tac.Enum.fst
LowParse.Spec.Base.parser_kind Prims.eqtype LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.serializer32 LowParse.Spec.Enum.enum Prims.b2t Prims.uu___is_Cons FStar.Pervasives.Native.tuple2 Prims.unit FStar.Tactics.V1.Derived.iseq Prims.Cons LowParse.TacLib.solve_vc LowParse.Spec.Tac.Enum.enum_repr_of_key_tac Prims.Nil LowParse.SLow.Tac.Enum.apply FStar.Reflection.Types.term LowParse.SLow.Enum.serialize32_maybe_enum_key_gen
module LowParse.SLow.Tac.Enum
include LowParse.Spec.Tac.Enum
include LowParse.SLow.Enum

module T = LowParse.TacLib

//
// The enum tactic solves goals of type ?u:eqtype with enum types that are
//   in the environment at type Type0
// So typechecking such uvars fails since F* 2635 bug fix
//   (since uvar solutions are checked with smt off)
//
// To circumvent that, we use t_apply with tc_resolve_uvars flag on,
//   so that ?u will be typechecked as soon as it is resolved,
//   resulting in an smt guard that will be added to the proofstate
//

let apply (t:T.term) : T.Tac unit =
  T.t_apply true false true t

noextract
let parse32_maybe_enum_key_tac
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (p32: parser32 p)
  (e: enum key repr { Cons? e } )
  ()
: T.Tac unit
= let fu = quote (parse32_maybe_enum_key_gen #k #key #repr #p p32 e) in
  apply fu;
  T.iseq [
    T.solve_vc;
    T.solve_vc;
    T.solve_vc;
    (fun () -> maybe_enum_key_of_repr_tac #key #repr e);
  ]

noextract
let parse32_enum_key_tac
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (p32: parser32 p)
  (e: enum key repr)
  ()
: T.Tac unit
= T.tassert (Cons? e);
  let fu = quote (parse32_enum_key_gen #k #key #repr p e) in
  apply fu;
  T.iseq [
    T.solve_vc;
    T.solve_vc;
    T.solve_vc;
    (fun () -> parse32_maybe_enum_key_tac p32 e ())
  ]

noextract
let serialize32_enum_key_gen_tac
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (#s: serializer p)
  (s32: serializer32 s)
  (e: enum key repr { Cons? e } )
  ()
: T.Tac unit
= let fu = quote (serialize32_enum_key_gen #k #key #repr #p #s s32 e) in
  apply fu;
  T.iseq [
    T.solve_vc;
    T.solve_vc;
    T.solve_vc;
    T.solve_vc;
    (fun () -> enum_repr_of_key_tac e);
  ]

noextract
let serialize32_maybe_enum_key_tac
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (#s: serializer p)
  (s32: serializer32 s)
  (e: enum key repr { Cons? e } )
  ()
val serialize32_maybe_enum_key_tac:
    #k: parser_kind ->
    #key: eqtype ->
    #repr: eqtype ->
    #p: parser k repr ->
    #s: serializer p ->
    s32: serializer32 s ->
    e: enum key repr {Cons? e} ->
    Prims.unit
  -> T.Tac unit

    s32: LowParse.SLow.Base.serializer32 s ->
    e: LowParse.Spec.Enum.enum key repr {Cons? e} ->
    _: Prims.unit
  -> FStar.Tactics.Effect.Tac Prims.unit