val serialize_nlist' (n: nat) (#t: Type0) (#p: parser_spec t) (s: serializer_spec p)
    : Tot (serializer_spec (parse_nlist n p))
val serialize_nlist' (n: nat) (#t: Type0) (#p: parser_spec t) (s: serializer_spec p)
    : Tot (serializer_spec (parse_nlist n p))
let rec serialize_nlist'
  (n: nat)
  (#t: Type0)
  (#p: parser_spec t)
  (s: serializer_spec p)
: Tot (serializer_spec (parse_nlist n p))
= if n = 0
  then begin
    Classical.forall_intro (nlist_nil_unique t);
    Serializer (fun _ -> Seq.empty)
  end
  else begin
    synth_inverse_1 t (n - 1);
    synth_inverse_2 t (n - 1);
    serialize_synth (serialize_nondep_then s (serialize_nlist' (n - 1) s)) (synth_nlist (n - 1)) (synth_nlist_recip (n - 1)) ()
  end
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module MiniParse.Spec.List
include MiniParse.Spec.Combinators // for seq_slice_append_l

module Seq = FStar.Seq
module L = FStar.List.Tot
module U32 = FStar.UInt32
module Classical = FStar.Classical

// inline_for_extraction
type nlist (n: nat) (t: Type) = (l: list t { L.length l == n } )

let nlist_nil (#t: Type) : Tot (nlist 0 t) = []

val nlist_nil_unique (t: Type) (l: nlist 0 t) : Lemma (l == nlist_nil)

let nlist_cons (#t: Type) (#n: nat) (a: t) (q: nlist n t) : Tot (nlist (n + 1) t) =
  a :: q

let nlist_destruct (#t: Type) (#n: nat) (x: nlist (n + 1) t) : Tot (t * nlist n t) =
  let (a :: q) = x in
  a, q

val nlist_cons_unique (#t: Type) (#n: nat) (x: nlist (n + 1) t) : Lemma
  (let (a, q) = nlist_destruct x in x == nlist_cons a q)

unfold let mul = Prims.op_Multiply

let synth_nlist (#t: Type) (n: nat) (xy: t * nlist n t) : Tot (nlist (n + 1) t) =
  let (x, y) = xy in
  nlist_cons x y

let synth_nlist_recip (#t: Type) (n: nat) (xy: nlist (n + 1) t) : Tot (t * nlist n t) =
  nlist_destruct xy

val synth_inverse_1 (t: Type) (n: nat) : Lemma
  (synth_inverse (synth_nlist #t n) (synth_nlist_recip n))

val synth_inverse_2 (t: Type) (n: nat) : Lemma
  (synth_inverse (synth_nlist_recip #t n) (synth_nlist n))

let rec parse_nlist'
  (n: nat)
  (#t: Type0)
  (p: parser_spec t)
: Tot (parser_spec (nlist n t))
= if n = 0
  then parse_ret nlist_nil
  else begin
    parse_synth
      (p `nondep_then` parse_nlist' (n - 1) p)
      (synth_nlist (n - 1))
      (synth_nlist_recip (n - 1))
  end

val parse_nlist
  (n: nat)
  (#t: Type0)
  (p: parser_spec t)
: Tot (y: parser_spec (nlist n t) { y == parse_nlist' n p } )

let parse_nlist_eq
  (n: nat)
  (#t: Type0)
  (p: parser_spec t)
  (b: bytes)
: Tot (squash (
  parse (parse_nlist n p) b == (
    if n = 0
    then Some ([], 0)
    else match parse p b with
    | Some (elem, consumed) ->
      let b' = Seq.slice b consumed (Seq.length b) in
      begin match parse (parse_nlist (n - 1) p) b' with
      | Some (q, consumed') -> Some (elem :: q, consumed + consumed')
      | _ -> None
      end
    | _ -> None
  )))
= if n = 0
  then ()
  else begin
    parse_synth_eq
      (p `nondep_then` parse_nlist' (n - 1) p)
      (synth_nlist (n - 1))
      (synth_nlist_recip (n - 1))
      b;
    nondep_then_eq p (parse_nlist' (n - 1) p) b
  end
/
prims.fst.checked MiniParse.Spec.Combinators.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
MiniParse.Spec.List.fsti
n: Prims.nat -> s: MiniParse.Spec.Base.serializer_spec p
  -> MiniParse.Spec.Base.serializer_spec (MiniParse.Spec.List.parse_nlist n p)
Prims.nat MiniParse.Spec.Base.parser_spec MiniParse.Spec.Base.serializer_spec Prims.op_Equality Prims.int MiniParse.Spec.Base.Serializer MiniParse.Spec.List.nlist MiniParse.Spec.List.parse_nlist FStar.Seq.Base.empty MiniParse.Spec.Base.byte MiniParse.Spec.Base.bytes Prims.unit FStar.Classical.forall_intro Prims.eq2 MiniParse.Spec.List.nlist_nil MiniParse.Spec.List.nlist_nil_unique Prims.bool MiniParse.Spec.Combinators.serialize_synth FStar.Pervasives.Native.tuple2 Prims.op_Subtraction MiniParse.Spec.Combinators.nondep_then MiniParse.Spec.Combinators.serialize_nondep_then MiniParse.Spec.List.serialize_nlist' MiniParse.Spec.List.synth_nlist MiniParse.Spec.List.synth_nlist_recip MiniParse.Spec.List.synth_inverse_2 MiniParse.Spec.List.synth_inverse_1
let rec serialize_nlist' (n: nat) (#t: Type0) (#p: parser_spec t) (s: serializer_spec p)
    : Tot (serializer_spec (parse_nlist n p)) =
  
if n = 0
then
  (Classical.forall_intro (nlist_nil_unique t);
    Serializer (fun _ -> Seq.empty))
else
  (synth_inverse_1 t (n - 1);
    synth_inverse_2 t (n - 1);
    serialize_synth (serialize_nondep_then s (serialize_nlist' (n - 1) s))
      (synth_nlist (n - 1))
      (synth_nlist_recip (n - 1))
      ())