val 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
                (match parse (parse_nlist (n - 1) p) b' with
                  | Some (q, consumed') -> Some (elem :: q, consumed + consumed')
                  | _ -> None)
              | _ -> None)))
val 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
                (match parse (parse_nlist (n - 1) p) b' with
                  | Some (q, consumed') -> Some (elem :: q, consumed + consumed')
                  | _ -> None)
              | _ -> None)))
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
(*
   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 } )
/
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 -> p: MiniParse.Spec.Base.parser_spec t -> b: MiniParse.Spec.Base.bytes
  -> Prims.squash (MiniParse.Spec.Base.parse (MiniParse.Spec.List.parse_nlist n p) b ==
        (match n = 0 with
          | true -> FStar.Pervasives.Native.Some ([], 0)
          | _ ->
            (match MiniParse.Spec.Base.parse p b with
              | FStar.Pervasives.Native.Some
                #_
                (FStar.Pervasives.Native.Mktuple2 #_ #_ elem consumed) ->
                let b' = FStar.Seq.Base.slice b consumed (FStar.Seq.Base.length b) in
                (match MiniParse.Spec.Base.parse (MiniParse.Spec.List.parse_nlist (n - 1) p) b' with
                  | FStar.Pervasives.Native.Some
                    #_
                    (FStar.Pervasives.Native.Mktuple2 #_ #_ q consumed') ->
                    FStar.Pervasives.Native.Some (elem :: q, consumed + consumed')
                  | _ -> FStar.Pervasives.Native.None)
                <:
                FStar.Pervasives.Native.option (MiniParse.Spec.List.nlist n t *
                    MiniParse.Spec.Base.consumed_length b)
              | _ -> FStar.Pervasives.Native.None)
            <:
            FStar.Pervasives.Native.option (MiniParse.Spec.List.nlist n t *
                MiniParse.Spec.Base.consumed_length b)))
Prims.nat MiniParse.Spec.Base.parser_spec MiniParse.Spec.Base.bytes Prims.op_Equality Prims.int Prims.bool MiniParse.Spec.Combinators.nondep_then_eq MiniParse.Spec.List.nlist Prims.op_Subtraction MiniParse.Spec.List.parse_nlist' Prims.unit MiniParse.Spec.Combinators.parse_synth_eq FStar.Pervasives.Native.tuple2 Prims.op_Addition MiniParse.Spec.Combinators.nondep_then MiniParse.Spec.List.synth_nlist MiniParse.Spec.List.synth_nlist_recip Prims.squash Prims.eq2 FStar.Pervasives.Native.option MiniParse.Spec.Base.consumed_length MiniParse.Spec.Base.parse MiniParse.Spec.List.parse_nlist FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.Nil Prims.Cons FStar.Pervasives.Native.None FStar.Seq.Base.seq MiniParse.Spec.Base.byte FStar.Seq.Base.slice FStar.Seq.Base.length
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
                (match parse (parse_nlist (n - 1) p) b' with
                  | Some (q, consumed') -> Some (elem :: q, consumed + consumed')
                  | _ -> None)
              | _ -> None))) =
  
if n = 0
then ()
else
  (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)