val seq_seq_match
      (#t1 #t2: Type)
      (p: (t1 -> t2 -> vprop))
      (c: Seq.seq t1)
      (l: Seq.seq t2)
      (i j: nat)
    : Tot vprop
let seq_seq_match
  (#t1 #t2: Type)
  (p: t1 -> t2 -> vprop)
  (c: Seq.seq t1)
  (l: Seq.seq t2)
  (i j: nat)
: Tot vprop
= on_range (seq_seq_match_item p c l) i j
val seq_seq_match
      (#t1 #t2: Type)
      (p: (t1 -> t2 -> vprop))
      (c: Seq.seq t1)
      (l: Seq.seq t2)
      (i j: nat)
    : Tot vprop
let seq_seq_match
      (#t1 #t2: Type)
      (p: (t1 -> t2 -> vprop))
      (c: Seq.seq t1)
      (l: Seq.seq t2)
      (i j: nat)
    : Tot vprop =
on_range (seq_seq_match_item p c l) i j
Steel.ST.SeqMatch.fst.checked
Steel.ST.OnRange.fsti.checked Steel.ST.GenElim.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Steel.ST.SeqMatch.fst
Steel.Effect.Common.vprop FStar.Seq.Base.seq Prims.nat Steel.ST.OnRange.on_range Steel.ST.SeqMatch.seq_seq_match_item
module Steel.ST.SeqMatch
include Steel.ST.OnRange
open Steel.ST.GenElim

module Seq = FStar.Seq
module SZ = FStar.SizeT

(* `seq_list_match` describes how to match a sequence of low-level
values (the low-level contents of an array) with a list of high-level
values. `seq_list_match` is carefully designed to be usable within
(mutually) recursive definitions of matching functions on the type of
high-level values.  *)

[@@__reduce__]
let seq_list_match_nil0
  (#t: Type)
  (c: Seq.seq t)
: Tot vprop
= pure (c `Seq.equal` Seq.empty)

[@@__reduce__]
let seq_list_match_cons0
  (#t #t': Type)
  (c: Seq.seq t)
  (l: list t' { Cons? l })
  (item_match: (t -> (v': t' { v' << l }) -> vprop))
  (seq_list_match: (Seq.seq t -> (v': list t') -> (raw_data_item_match: (t -> (v'': t' { v'' << v' }) -> vprop) { v' << l }) ->
vprop))
: Tot vprop
= exists_ (fun (c1: t) -> exists_ (fun (c2: Seq.seq t) ->
    item_match c1 (List.Tot.hd l) `star`
    seq_list_match c2 (List.Tot.tl l) item_match `star`
    pure (c `Seq.equal` Seq.cons c1 c2)
  ))

let rec seq_list_match
  (#t #t': Type)
  (c: Seq.seq t)
  (v: list t')
  (item_match: (t -> (v': t' { v' << v }) -> vprop))
: Tot vprop
  (decreases v)
= if Nil? v
  then seq_list_match_nil0 c
  else seq_list_match_cons0 c v item_match seq_list_match

let seq_list_match_cons_eq
  (#t #t': Type)
  (c: Seq.seq t)
  (v: list t')
  (item_match: (t -> (v': t' { v' << v }) -> vprop))
: Lemma
  (requires (Cons? v))
  (ensures (
    seq_list_match c v item_match ==
    seq_list_match_cons0 c v item_match seq_list_match
  ))
= let a :: q = v in
  assert_norm (seq_list_match c (a :: q) item_match ==
    seq_list_match_cons0 c (a :: q) item_match seq_list_match
  )

// this one cannot be proven with seq_seq_match because of the << refinement in the type of item_match
let rec seq_list_match_weaken
  (#opened: _)
  (#t #t': Type)
  (c: Seq.seq t)
  (v: list t')
  (item_match1 item_match2: (t -> (v': t' { v' << v }) -> vprop))
  (prf: (
    (#opened: _) ->
    (c': t) ->
    (v': t' { v' << v }) ->
    STGhostT unit opened
      (item_match1 c' v')
      (fun _ -> item_match2 c' v')
  ))
: STGhostT unit opened
    (seq_list_match c v item_match1)
    (fun _ -> seq_list_match c v item_match2)
    (decreases v)
= if Nil? v
  then
    rewrite (seq_list_match c v item_match1) (seq_list_match c v item_match2)
  else begin
    let _ : squash (Cons? v) = () in
    seq_list_match_cons_eq c v item_match1;
    seq_list_match_cons_eq c v item_match2;
    rewrite
      (seq_list_match c v item_match1)
      (seq_list_match_cons0 c v item_match1 seq_list_match);
    let _ = gen_elim () in
    prf _ _;
    seq_list_match_weaken _ (List.Tot.tl v) item_match1 item_match2 prf;
    rewrite
      (seq_list_match_cons0 c v item_match2 seq_list_match)
      (seq_list_match c v item_match2)
  end

(* `seq_seq_match` describes how to match a sequence of low-level
values (the low-level contents of an array) with a sequence of high-level
values. Contrary to `seq_list_match`, `seq_seq_match` is not meant to be usable within
(mutually) recursive definitions of matching functions on the type of
high-level values, because no lemma ensures that `Seq.index s i << s`  *)

let seq_seq_match_item
  (#t1 #t2: Type)
  (p: t1 -> t2 -> vprop)
  (c: Seq.seq t1)
  (l: Seq.seq t2)
  (i: nat)
: Tot vprop
= if i < Seq.length c && i < Seq.length l
  then
    p (Seq.index c i) (Seq.index l i)
  else
    pure (squash False)

let seq_seq_match_item_tail
  (#t1 #t2: Type)
  (p: t1 -> t2 -> vprop)
  (c: Seq.seq t1)
  (l: Seq.seq t2)
  (delta: nat)
  (i: nat)
: Lemma
  (requires (
    i + delta <= Seq.length c /\
    i + delta <= Seq.length l
  ))
  (ensures (
    seq_seq_match_item p (Seq.slice c delta (Seq.length c)) (Seq.slice l delta (Seq.length l)) i ==
      seq_seq_match_item p c l (i + delta)
  ))
= ()

[@@__reduce__]
let seq_seq_match
  (#t1 #t2: Type)
  (p: t1 -> t2 -> vprop)
  (c: Seq.seq t1)
  (l: Seq.seq t2)
  (i j: nat)
val seq_seq_match
      (#t1 #t2: Type)
      (p: (t1 -> t2 -> vprop))
      (c: Seq.seq t1)
      (l: Seq.seq t2)
      (i j: nat)
    : Tot vprop

    p: (_: t1 -> _: t2 -> Steel.Effect.Common.vprop) ->
    c: FStar.Seq.Base.seq t1 ->
    l: FStar.Seq.Base.seq t2 ->
    i: Prims.nat ->
    j: Prims.nat
  -> Steel.Effect.Common.vprop