From 169c528be787a23fd59c1899228416c6668459ab Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Thu, 16 Nov 2023 14:45:29 -0500
Subject: [PATCH] Support abi and where_clause

---
 examples/wip.rs     |  8 ++------
 src/lib.rs          | 19 ++++++++++---------
 src/verus.pest      |  9 +++++++--
 tests/snap-tests.rs |  8 ++++++++
 4 files changed, 27 insertions(+), 17 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index 8cc7544..0302fe9 100644
--- a/examples/wip.rs
+++ b/examples/wip.rs
@@ -1,11 +1,7 @@
 verus! {
 
-#[verifier(external_body)]
-pub struct NetClientCPointers {
-    get_time_func: extern "C" fn() -> u64,
-    receive_func: extern "C" fn(i32, *mut bool, *mut bool, *mut *mut std::vec::Vec<u8>, *mut *mut std::vec::Vec<u8>),
-    send_func: extern "C" fn(u64, *const u8, u64, *const u8) -> bool
+trait KeyTrait: Sized {
+    fn zero_spec() -> Self where Self: std::marker::Sized;
 }
 
-
 } // verus!
diff --git a/src/lib.rs b/src/lib.rs
index 81a47a8..95c761d 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -176,7 +176,7 @@ fn sticky_delims<'a>(
         Parens => ")",
     };
     let closing_space = match enc {
-        Braces => arena.line(), //.text(" "),
+        Braces => arena.line(), //.space(),
         Brackets => arena.nil(),
         Parens => arena.nil(),
     };
@@ -637,7 +637,7 @@ fn to_doc<'a>(
                 }
             }))
         }
-        Rule::abi => map_to_doc(ctx, arena, pair).append(arena.text(" ")),
+        Rule::abi => map_to_doc(ctx, arena, pair).append(arena.space()),
         Rule::param_list => comma_delimited(ctx, arena, pair).parens().group(),
         Rule::closure_param_list => comma_delimited(ctx, arena, pair)
             .enclose(arena.text("|"), arena.text("|"))
@@ -690,7 +690,7 @@ fn to_doc<'a>(
                             d
                         }
                     }
-                    Rule::for_str => arena.text(" ").append(d),
+                    Rule::for_str => arena.space().append(d),
                     _ => d,
                 }
             }))
@@ -704,8 +704,9 @@ fn to_doc<'a>(
         Rule::type_param => map_to_doc(ctx, arena, pair),
         Rule::const_param => unsupported(pair),
         Rule::lifetime_param => map_to_doc(ctx, arena, pair),
-        Rule::where_clause => unsupported(pair),
-        Rule::where_pred => unsupported(pair),
+        Rule::where_clause => arena.space().append(map_to_doc(ctx, arena, pair)),
+        Rule::where_preds => comma_delimited(ctx, arena, pair).group(),
+        Rule::where_pred => map_to_doc(ctx, arena, pair),
         Rule::visibility => s.append(arena.space()),
         Rule::attr_core => arena.text(pair.as_str()),
         Rule::attr => map_to_doc(ctx, arena, pair).append(arena.hardline()),
@@ -794,7 +795,7 @@ fn to_doc<'a>(
                         Rule::attr_inner => arena
                             .line_()
                             .append(to_doc(ctx, p, arena))
-                            .append(arena.nil().flat_alt(arena.text(" ")))
+                            .append(arena.nil().flat_alt(arena.space()))
                             .nest(INDENT_SPACES),
                         _ => to_doc(ctx, p, arena),
                     }
@@ -805,8 +806,8 @@ fn to_doc<'a>(
         Rule::if_expr => map_to_doc(ctx, arena, pair),
         Rule::loop_expr => unsupported(pair),
         Rule::for_expr => arena.concat(pair.into_inner().map(|p| match p.as_rule() {
-            Rule::in_str => arena.text(" ").append(to_doc(ctx, p, arena)),
-            Rule::expr_no_struct => to_doc(ctx, p, arena).append(arena.text(" ")),
+            Rule::in_str => arena.space().append(to_doc(ctx, p, arena)),
+            Rule::expr_no_struct => to_doc(ctx, p, arena).append(arena.space()),
             _ => to_doc(ctx, p, arena),
         })),
         Rule::while_expr => {
@@ -897,7 +898,7 @@ fn to_doc<'a>(
         Rule::end_only_range_pat => map_to_doc(ctx, arena, pair),
         Rule::ref_pat => arena.text("&").append(map_to_doc(ctx, arena, pair)),
         Rule::record_pat => arena.concat(pair.into_inner().map(|p| match p.as_rule() {
-            Rule::path => to_doc(ctx, p, arena).append(arena.text(" ")),
+            Rule::path => to_doc(ctx, p, arena).append(arena.space()),
             _ => to_doc(ctx, p, arena),
         })),
         Rule::record_pat_field_list => {
diff --git a/src/verus.pest b/src/verus.pest
index a294907..b6054ef 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -536,7 +536,7 @@ use_tree_list = {
 }
 
 fn_qualifier = {
-    prover? ~ where_clause? ~ (requires_clause | recommends_clause | ensures_clause | decreases_clause)*
+    (requires_clause | recommends_clause | ensures_clause | decreases_clause)*
 }
 
 fn_terminator = {
@@ -548,6 +548,7 @@ fn = {
     attr* ~ visibility? ~ publish? ~
     default_str? ~ const_str? ~ async_str? ~ unsafe_str? ~ abi? ~ fn_mode? ~
     fn_str ~ name ~ generic_param_list? ~ param_list ~ ret_type? ~
+    prover? ~ where_clause? ~
     fn_qualifier ~
     fn_terminator
 }
@@ -744,7 +745,11 @@ lifetime_param = {
 }
 
 where_clause = {
-    where_str ~ (where_pred ~ ("," ~ where_pred)* ~ ","?)?
+    where_str ~ where_preds?
+}
+
+where_preds = {
+    where_pred ~ ("," ~ where_pred)* ~ ","?
 }
 
 where_pred = {
diff --git a/tests/snap-tests.rs b/tests/snap-tests.rs
index 839c960..84934ad 100644
--- a/tests/snap-tests.rs
+++ b/tests/snap-tests.rs
@@ -489,6 +489,10 @@ trait T {
     ;
 }
 
+trait KeyTrait: Sized {
+    fn zero_spec() -> Self where Self: std::marker::Sized;
+}
+
 }
 "#;
 
@@ -506,6 +510,10 @@ trait T {
         ;
     }
 
+    trait KeyTrait: Sized {
+        fn zero_spec() -> Self where Self: std::marker::Sized;
+    }
+
     } // verus!
     "###);
 }