Merge pull request #3203 from mtzguido/seq

Seq: reimplement seq_to_list and seq_of_list by casting

tests/ide/emacs/search.cons-snoc.out.expected

@@ -1,4 +1,4 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": [], "status": "success"}
-{"contents": "* Error 147 at FStar.Seq.Properties.fsti(774,0-776,62):\n  - Effect template STATE_h should be applied to arguments for its binders ((heap: Type)) before it can be used at an effect position\n  - See also <input>(1,0-1,0)\n\n", "kind": "message", "level": "error", "query-id": "2"}
+{"contents": "* Error 147 at FStar.Seq.Properties.fsti(760,0-762,62):\n  - Effect template STATE_h should be applied to arguments for its binders ((heap: Type)) before it can be used at an effect position\n  - See also <input>(1,0-1,0)\n\n", "kind": "message", "level": "error", "query-id": "2"}
 {"contents": "1 error was reported (see above)\n", "kind": "message", "level": "error", "query-id": "2"}

ulib/FStar.Endianness.fst

@@ -280,16 +280,30 @@ let le_of_seq_uint32_base s1 s2 = ()
 let be_of_seq_uint64_base s1 s2 = ()
 
 let rec be_of_seq_uint32_append s1 s2 =
-  Classical.forall_intro_2 (tail_cons #U32.t); // TODO: this is a local pattern, remove once tail_cons lands in FStar.Seq.Properties
   if S.length s1 = 0 then begin
     assert (S.equal (be_of_seq_uint32 s1) S.empty);
+    assert (S.equal s1 S.empty);
+    S.append_empty_l s2;
+    S.append_empty_l (be_of_seq_uint32 s2);
     assert (S.equal (S.append s1 s2) s2);
     ()
   end else begin
-    assert (S.equal (S.append s1 s2) (S.cons (S.head s1) (S.append (S.tail s1) s2)));
-    assert (S.equal (be_of_seq_uint32 (S.append s1 s2))
-      (S.append (be_of_uint32 (S.head s1)) (be_of_seq_uint32 (S.append (S.tail s1) s2))));
-    be_of_seq_uint32_append (S.tail s1) s2
+    calc S.equal {
+      be_of_seq_uint32 (S.append s1 s2);
+      S.equal { () }
+      be_of_seq_uint32 (S.append (S.cons (S.head s1) (S.tail s1)) s2);
+      S.equal { S.append_cons (S.head s1) (S.tail s1) s2 }
+      be_of_seq_uint32 (S.cons (S.head s1) (S.append (S.tail s1) s2));
+      S.equal { () }
+      be_of_seq_uint32 (S.cons (S.head s1) (S.append (S.tail s1) s2));
+      S.equal { S.head_cons (S.head s1) (S.append (S.tail s1) s2);
+                tail_cons (S.head s1) (S.append (S.tail s1) s2) }
+      S.append (be_of_uint32 (S.head s1))
+               (be_of_seq_uint32 (S.append (S.tail s1) s2));
+      S.equal { be_of_seq_uint32_append (S.tail s1) s2 }
+      S.append (be_of_uint32 (S.head s1))
+               (S.append (be_of_seq_uint32 (S.tail s1)) (be_of_seq_uint32 s2));
+    }
   end
 
 let rec le_of_seq_uint32_append s1 s2 =

ulib/FStar.Seq.Base.fst

@@ -25,22 +25,28 @@ type seq (a:Type u#a) :Type u#a =
 
 let length #_ s = List.length (MkSeq?.l s)
 
+let seq_to_list #_ s =
+  match s with
+  | MkSeq l -> l
+
+let seq_of_list #_ l = MkSeq l
+
 let index #_ s i = List.index (MkSeq?.l s) i
 
-let cons (#a:Type) (x:a) (s:seq a) : Tot (seq a) = MkSeq (x::(MkSeq?.l s))
+let _cons (#a:Type) (x:a) (s:seq a) : Tot (seq a) = MkSeq (x::(MkSeq?.l s))
 
 let hd (#a:Type) (s:seq a{length s > 0}) : Tot a = List.hd (MkSeq?.l s)
 
 let tl (#a:Type) (s:seq a{length s > 0}) : Tot (seq a) = MkSeq (List.tl (MkSeq?.l s))
 
-let rec create #_ len v = if len = 0 then MkSeq [] else cons v (create (len - 1) v)
+let rec create #_ len v = if len = 0 then MkSeq [] else _cons v (create (len - 1) v)
 
 private let rec init_aux' (#a:Type) (len:nat) (k:nat{k < len}) (contents: (i:nat{i < len} -> Tot a))
     : Tot (seq a)
       (decreases (len - k))
   = if k + 1 = len
     then MkSeq [contents k]
-    else cons (contents k) (init_aux' len (k+1) contents)
+    else _cons (contents k) (init_aux' len (k+1) contents)
 
 let init_aux = init_aux'
 
@@ -51,7 +57,7 @@ private let rec init_aux_ghost' (#a:Type) (len:nat) (k:nat{k < len}) (contents:(
       (decreases (len - k))
   = if k + 1 = len
     then MkSeq [contents k]
-    else cons (contents k) (init_aux_ghost' len (k+1) contents)
+    else _cons (contents k) (init_aux_ghost' len (k+1) contents)
 
 let init_aux_ghost = init_aux_ghost'
 
@@ -64,7 +70,7 @@ let lemma_empty #_ _ = ()
 private let rec upd' (#a:Type) (s:seq a) (n:nat{n < length s}) (v:a)
     : Tot (seq a)
       (decreases (length s))
-  = if n = 0 then cons v (tl s) else cons (hd s) (upd' (tl s) (n - 1) v)
+  = if n = 0 then _cons v (tl s) else _cons (hd s) (upd' (tl s) (n - 1) v)
 
 let upd = upd'
 
@@ -75,10 +81,15 @@ private let rec slice' (#a:Type) (s:seq a) (i:nat) (j:nat{i <= j && j <= length
       (decreases (length s))
   =  if i > 0 then slice' #a (tl s) (i - 1) (j - 1)
      else if j = 0 then MkSeq []
-          else cons (hd s) (slice' #a (tl s) i (j - 1))
+          else _cons (hd s) (slice' #a (tl s) i (j - 1))
 
 let slice = slice'
 
+let lemma_seq_of_seq_to_list #_ s = ()
+let lemma_seq_to_seq_of_list #_ s = ()
+let lemma_seq_of_list_cons #_ x l = ()
+let lemma_seq_to_list_cons #_ x s = ()
+
 let rec lemma_create_len #_ n i = if n = 0 then () else lemma_create_len (n - 1) i
 
 let rec lemma_init_aux_len' (#a:Type) (n:nat) (k:nat{k < n}) (contents:(i:nat{ i < n } -> Tot a))

ulib/FStar.Seq.Base.fsti

@@ -25,6 +25,10 @@ new val seq ([@@@strictly_positive] a : Type u#a) : Type u#a
 (* Destructors *)
 val length: #a:Type -> seq a -> Tot nat
 
+val seq_to_list (#a:Type) (s:seq a) : Tot (l:list a{List.length l == length s})
+
+val seq_of_list (#a:Type) (l:list a) : Tot (s:seq a{List.length l == length s})
+
 val index:  #a:Type -> s:seq a -> i:nat{i < length s} -> Tot a
 
 val create: #a:Type -> nat -> a -> Tot (seq a)
@@ -53,10 +57,37 @@ val upd: #a:Type -> s:seq a -> n:nat{n < length s} -> a ->  Tot (seq a)
 
 val append: #a:Type -> seq a -> seq a -> Tot (seq a)
 
+let cons (#a:Type) (x:a) (s:seq a) : Tot (seq a) = append (create 1 x) s
+
 let op_At_Bar (#a:Type) (s1:seq a) (s2:seq a) = append s1 s2
 
 val slice:  #a:Type -> s:seq a -> i:nat -> j:nat{i <= j && j <= length s} -> Tot (seq a)
 
+(* Lemmas about seq_to_list/seq_of_list *)
+val lemma_seq_of_seq_to_list : #a:Type -> s:seq a ->
+  Lemma
+  (requires True)
+  (ensures seq_of_list (seq_to_list s) == s)
+  [SMTPat (seq_of_list (seq_to_list s))]
+
+val lemma_seq_to_seq_of_list : #a:Type -> l:list a ->
+  Lemma
+  (requires True)
+  (ensures seq_to_list (seq_of_list l) == l)
+  [SMTPat (seq_to_list (seq_of_list l))]
+
+val lemma_seq_of_list_cons : #a:Type -> x:a -> l:list a ->
+  Lemma
+  (requires True)
+  (ensures seq_of_list (x::l) == create 1 x @| seq_of_list l)
+  [SMTPat (seq_of_list (x::l))]
+
+val lemma_seq_to_list_cons : #a:Type -> x:a -> s:seq a ->
+  Lemma
+  (requires True)
+  (ensures seq_to_list (cons x s) == x :: seq_to_list s)
+  [SMTPat (seq_to_list (cons x s))]
+
 (* Lemmas about length *)
 val lemma_create_len: #a:Type -> n:nat -> i:a -> Lemma
   (requires True)