Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable DeepModel derive to work with generic parameters #906

Closed
wants to merge 1 commit into from
Closed

Enable DeepModel derive to work with generic parameters #906

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

14 changes: 7 additions & 7 deletions creusot-contracts-proc/src/derive/deep_model.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use proc_macro2::{Ident, TokenStream};
use quote::{format_ident, quote, quote_spanned};
use syn::{
parse_macro_input, parse_quote, spanned::Spanned, Data, DeriveInput, Error, Expr, ExprLit,
Fields, GenericParam, Generics, Index, Lit, Meta, MetaNameValue, Path,
Fields, GenericParam, Generics, Index, Lit, Meta, MetaNameValue, Path, TypeGenerics, WhereClause, ImplGenerics,
};

pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
Expand All @@ -28,17 +28,17 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
&format!("{}DeepModel", name.to_string()),
proc_macro::Span::def_site().into(),
);
let deep_model_ty = deep_model_ty(&ident, &generics, &input.data);
let deep_model_ty = deep_model_ty(&ident, &impl_generics, &input.data);

(ident.into(), Some(quote! { #vis #deep_model_ty}))
};

let eq = deep_model(&name, &deep_model_ty_name, &input.data);

let open = match vis {
syn::Visibility::Public(_) => quote! {#[open]},
syn::Visibility::Restricted(res) => quote! { #[open(#res)] },
syn::Visibility::Inherited => quote! { #[open(self)] },
syn::Visibility::Public(_) => quote! {#[creusot_contracts::open]},
syn::Visibility::Restricted(res) => quote! { #[creusot_contracts::open(#res)] },
syn::Visibility::Inherited => quote! { #[creusot_contracts::open(self)] },
};

let expanded = quote! {
Expand All @@ -47,7 +47,7 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
impl #impl_generics ::creusot_contracts::DeepModel for #name #ty_generics #where_clause {
type DeepModelTy = #deep_model_ty_name #ty_generics;

#[ghost]
#[creusot_contracts::ghost]
#open
fn deep_model(self) -> Self::DeepModelTy {
#eq
Expand Down Expand Up @@ -113,7 +113,7 @@ fn deep_model_ty_fields(fields: &Fields) -> TokenStream {
}
}

fn deep_model_ty(base_ident: &Ident, generics: &Generics, data: &Data) -> TokenStream {
fn deep_model_ty(base_ident: &Ident, generics : &ImplGenerics, data: &Data) -> TokenStream {
match data {
Data::Struct(ref data) => {
let data = deep_model_ty_fields(&data.fields);
Expand Down
2 changes: 1 addition & 1 deletion creusot-contracts-proc/src/derive/partial_eq.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ pub fn derive_partial_eq(input: proc_macro::TokenStream) -> proc_macro::TokenStr

let expanded = quote! {
impl #impl_generics ::std::cmp::PartialEq for #name #ty_generics #where_clause {
#[ensures(result == (::creusot_contracts::model::DeepModel::deep_model(self) ==
#[creusot_contracts::ensures(result == (::creusot_contracts::model::DeepModel::deep_model(self) ==
::creusot_contracts::model::DeepModel::deep_model(rhs)))]
fn eq(&self, rhs: &Self) -> bool {
#eq
Expand Down
6 changes: 6 additions & 0 deletions creusot-contracts/src/num_rational.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,13 @@
use std::marker::PhantomData;

<<<<<<< Updated upstream
use crate::{ghost, open, trusted, DeepModel, OrdLogic};
use num_rational::BigRational;
=======
use crate::{ghost, open, trusted, DeepModel, ShallowModel, Int, OrdLogic};
use num_rational::{BigRational};
pub use num::BigInt;
>>>>>>> Stashed changes
use std::cmp::Ordering;

#[cfg_attr(creusot, creusot::builtins = "prelude.Real.real")]
Expand Down
2 changes: 2 additions & 0 deletions mlcfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ cargo run --bin creusot-rustc -- \
--span-mode=absolute \
-- -Zno-codegen \
-Zmacro-backtrace \
--edition=2018 \
--extern num=./target/debug/lib_num.rlib \
--extern creusot_contracts=./target/debug/libcreusot_contracts.rlib \
-Ldependency=./target/debug/deps/ \
--crate-type=lib \
Expand Down
Loading