val parse_list_up_to_fuel
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
    : Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)) (decreases fuel)
let rec parse_list_up_to_fuel
  (#k: parser_kind)
  (#t: Type)
  (cond: (t -> Tot bool))
  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
  (fuel: nat)
: Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
  (decreases fuel)
= if fuel = 0
  then fail_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)
  else
    parse_dtuple2
      (weaken (parse_list_up_to_kind k) p)
      #(parse_list_up_to_payload_kind k)
      #(parse_list_up_to_payload_t cond (fuel - 1))
      (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
      `parse_synth`
      synth_list_up_to_fuel cond (fuel - 1)
val parse_list_up_to_fuel
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
    : Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)) (decreases fuel)
let rec parse_list_up_to_fuel
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
    : Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)) (decreases fuel) =
if fuel = 0
then fail_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)
else
  (parse_dtuple2 (weaken (parse_list_up_to_kind k) p)
      #(parse_list_up_to_payload_kind k)
      #(parse_list_up_to_payload_t cond (fuel - 1))
      (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1))))
  `parse_synth`
  (synth_list_up_to_fuel cond (fuel - 1))
LowParse.Spec.ListUpTo.fst.checked
prims.fst.checked LowParse.Spec.Seq.fst.checked LowParse.Spec.Fuel.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.ListUpTo.fst
LowParse.Spec.Base.parser_kind Prims.bool LowParse.Spec.Base.parser Prims.b2t Prims.op_disEquality FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserConsumesAll Prims.nat Prims.op_Equality Prims.int LowParse.Spec.Combinators.fail_parser LowParse.Spec.ListUpTo.parse_list_up_to_kind LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.and_then_kind LowParse.Spec.ListUpTo.parse_list_up_to_payload_kind Prims.dtuple2 LowParse.Spec.ListUpTo.parse_list_up_to_payload_t Prims.op_Subtraction LowParse.Spec.Combinators.parse_dtuple2 LowParse.Spec.Base.weaken LowParse.Spec.ListUpTo.parse_list_up_to_payload LowParse.Spec.ListUpTo.parse_list_up_to_fuel LowParse.Spec.ListUpTo.synth_list_up_to_fuel
module LowParse.Spec.ListUpTo
open LowParse.Spec.Base
open LowParse.Spec.Fuel
open LowParse.Spec.Combinators

let llist
  (t: Type)
  (fuel: nat)
: Tot Type
= (l: list t { L.length l < fuel })

let parse_list_up_to_fuel_t
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
: Tot Type
= (llist (refine_with_cond (negate_cond cond)) fuel) & refine_with_cond cond

(* Universe-polymorphic unit type *)
type up_unit : Type u#r = | UP_UNIT

let parse_list_up_to_payload_t
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (x: t)
: Tot Type
= if cond x
  then up_unit
  else parse_list_up_to_fuel_t cond fuel

let synth_list_up_to_fuel
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (xy: dtuple2 t (parse_list_up_to_payload_t cond fuel))
: Tot (parse_list_up_to_fuel_t cond (fuel + 1))
= let (| x, yz |) = xy in
  if cond x
  then ([], x)
  else
    let (y, z) = (yz <: parse_list_up_to_fuel_t cond fuel) in
    (x :: y, z)

let synth_list_up_to_injective
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
: Lemma
  (synth_injective (synth_list_up_to_fuel cond fuel))
  [SMTPat (synth_injective (synth_list_up_to_fuel cond fuel))]
= ()

inline_for_extraction
let parse_list_up_to_payload_kind (k: parser_kind) : Tot (k' : parser_kind {k' `is_weaker_than` k }) = {
  parser_kind_low = 0;
  parser_kind_high = None;
  parser_kind_subkind = k.parser_kind_subkind;
  parser_kind_metadata = None;
}

let parse_list_up_to_payload
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (k: parser_kind { k.parser_kind_subkind <> Some ParserConsumesAll })
  (ptail: parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
  (x: t)
: Tot (parser (parse_list_up_to_payload_kind k) (parse_list_up_to_payload_t cond fuel x))
= if cond x
  then weaken (parse_list_up_to_payload_kind k) (parse_ret UP_UNIT)
  else weaken (parse_list_up_to_payload_kind k) ptail

let rec parse_list_up_to_fuel
  (#k: parser_kind)
  (#t: Type)
  (cond: (t -> Tot bool))
  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
  (fuel: nat)
: Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
val parse_list_up_to_fuel
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
    : Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)) (decreases fuel)

    cond: (_: t -> Prims.bool) ->
    p:
      LowParse.Spec.Base.parser k t
        { Mkparser_kind'?.parser_kind_subkind k <>
          FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserConsumesAll } ->
    fuel: Prims.nat
  -> Prims.Tot
    (LowParse.Spec.Base.parser (LowParse.Spec.ListUpTo.parse_list_up_to_kind k)
        (LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t cond fuel))