Implement ToView for request types (#308)

Signed-off-by: Xudong Sun <[email protected]>

src/controller_examples/rabbitmq_controller/exec/reconciler.rs

@@ -13,8 +13,7 @@ use crate::rabbitmq_controller::exec::types::*;
 use crate::rabbitmq_controller::spec::reconciler as rabbitmq_spec;
 use crate::rabbitmq_controller::spec::resource as spec_resource;
 use crate::reconciler::exec::{io::*, reconciler::*};
-use crate::vstd_ext::string_map::StringMap;
-use crate::vstd_ext::string_view::*;
+use crate::vstd_ext::{string_map::StringMap, string_view::*, to_view::*};
 use vstd::prelude::*;
 use vstd::seq_lib::*;
 use vstd::string::*;

src/controller_examples/rabbitmq_controller/exec/resource/common.rs

@@ -11,8 +11,7 @@ use crate::rabbitmq_controller::common::*;
 use crate::rabbitmq_controller::exec::types::*;
 use crate::rabbitmq_controller::spec::resource as spec_resource;
 use crate::reconciler::exec::{io::*, reconciler::*};
-use crate::vstd_ext::string_map::StringMap;
-use crate::vstd_ext::string_view::*;
+use crate::vstd_ext::{string_map::StringMap, string_view::*, to_view::*};
 use vstd::prelude::*;
 use vstd::seq_lib::*;
 use vstd::string::*;

src/kubernetes_api_objects/api_method.rs

@@ -122,7 +122,15 @@ pub struct KubeGetRequest {
 }
 
 impl KubeGetRequest {
-    pub open spec fn to_view(&self) -> GetRequest {
+    #[verifier(external)]
+    pub fn key(&self) -> std::string::String {
+        format!("{}/{}/{}", self.api_resource.as_kube_ref().kind, self.namespace.as_rust_string_ref(), self.name.as_rust_string_ref())
+    }
+}
+
+impl ToView for KubeGetRequest {
+    type V = GetRequest;
+    open spec fn to_view(&self) -> GetRequest {
         GetRequest {
             key: ObjectRef {
                 kind: self[email protected],
@@ -133,13 +141,6 @@ impl KubeGetRequest {
     }
 }
 
-impl KubeGetRequest {
-    #[verifier(external)]
-    pub fn key(&self) -> std::string::String {
-        format!("{}/{}/{}", self.api_resource.as_kube_ref().kind, self.namespace.as_rust_string_ref(), self.name.as_rust_string_ref())
-    }
-}
-
 /// KubeListRequest has the namespace to instantiate an Api.
 ///
 /// Note that the kind is indicated by the upper layer Kube{ObjectKind}Request.
@@ -156,6 +157,16 @@ impl KubeListRequest {
     }
 }
 
+impl ToView for KubeListRequest {
+    type V = ListRequest;
+    open spec fn to_view(&self) -> ListRequest {
+        ListRequest {
+            kind: self[email protected],
+            namespace: self.namespace@,
+        }
+    }
+}
+
 /// KubeCreateRequest has the obj as the parameter of Api.create().
 
 pub struct KubeCreateRequest {
@@ -171,6 +182,16 @@ impl KubeCreateRequest {
     }
 }
 
+impl ToView for KubeCreateRequest {
+    type V = CreateRequest;
+    open spec fn to_view(&self) -> CreateRequest {
+        CreateRequest {
+            namespace: self.namespace@,
+            obj: self.obj@,
+        }
+    }
+}
+
 /// KubeDeleteRequest has the name as the parameter of Api.delete(), and namespace to instantiate an Api.
 
 pub struct KubeDeleteRequest {
@@ -186,6 +207,19 @@ impl KubeDeleteRequest {
     }
 }
 
+impl ToView for KubeDeleteRequest {
+    type V = DeleteRequest;
+    open spec fn to_view(&self) -> DeleteRequest {
+        DeleteRequest {
+            key: ObjectRef {
+                kind: self[email protected],
+                name: self.name@,
+                namespace: self.namespace@,
+            }
+        }
+    }
+}
+
 /// KubeUpdateRequest has the obj as the parameter of Api.replace().
 
 pub struct KubeUpdateRequest {
@@ -202,6 +236,17 @@ impl KubeUpdateRequest {
     }
 }
 
+impl ToView for KubeUpdateRequest {
+    type V = UpdateRequest;
+    open spec fn to_view(&self) -> UpdateRequest {
+        UpdateRequest {
+            name: self.name@,
+            namespace: self.namespace@,
+            obj: self.obj@,
+        }
+    }
+}
+
 /// KubeUpdateRequest has the obj as the parameter of Api.replace_status().
 
 pub struct KubeUpdateStatusRequest {
@@ -218,35 +263,26 @@ impl KubeUpdateStatusRequest {
     }
 }
 
+impl ToView for KubeUpdateStatusRequest {
+    type V = UpdateStatusRequest;
+    open spec fn to_view(&self) -> UpdateStatusRequest {
+        UpdateStatusRequest {
+            name: self.name@,
+            namespace: self.namespace@,
+            obj: self.obj@,
+        }
+    }
+}
+
 impl KubeAPIRequest {
     pub open spec fn to_view(&self) -> APIRequest {
         match self {
             KubeAPIRequest::GetRequest(get_req) => APIRequest::GetRequest(get_req.to_view()),
-            KubeAPIRequest::ListRequest(list_req) => APIRequest::ListRequest(ListRequest {
-                kind: [email protected],
-                namespace: list_req.namespace@,
-            }),
-            KubeAPIRequest::CreateRequest(create_req) => APIRequest::CreateRequest(CreateRequest {
-                namespace: create_req.namespace@,
-                obj: create_req.obj@,
-            }),
-            KubeAPIRequest::DeleteRequest(delete_req) => APIRequest::DeleteRequest(DeleteRequest {
-                key: ObjectRef {
-                    kind: [email protected],
-                    name: delete_req.name@,
-                    namespace: delete_req.namespace@,
-                }
-            }),
-            KubeAPIRequest::UpdateRequest(update_req) => APIRequest::UpdateRequest(UpdateRequest {
-                name: update_req.name@,
-                namespace: update_req.namespace@,
-                obj: update_req.obj@,
-            }),
-            KubeAPIRequest::UpdateStatusRequest(update_status_req) => APIRequest::UpdateStatusRequest(UpdateStatusRequest {
-                name: update_status_req.name@,
-                namespace: update_status_req.namespace@,
-                obj: update_status_req.obj@,
-            }),
+            KubeAPIRequest::ListRequest(list_req) => APIRequest::ListRequest(list_req.to_view()),
+            KubeAPIRequest::CreateRequest(create_req) => APIRequest::CreateRequest(create_req.to_view()),
+            KubeAPIRequest::DeleteRequest(delete_req) => APIRequest::DeleteRequest(delete_req.to_view()),
+            KubeAPIRequest::UpdateRequest(update_req) => APIRequest::UpdateRequest(update_req.to_view()),
+            KubeAPIRequest::UpdateStatusRequest(update_status_req) => APIRequest::UpdateStatusRequest(update_status_req.to_view()),
         }
     }
 }