PhantomData is just a field-less marker, so it is safe to extract it as a field-less ADT.
The trick used here, is that we detect the
use std::marker::PhantomData
and extract it as
case class PhantomData[T]()
Closes #69.
The awesome thing is, that the existing extract_adt function also works for crate-external ADTs. (Therefore, the feature addition in the last commit of this PR is minimal effort.) This opens the door to using the real std::*::Option/Result/etc. Tracking that feature here: https://github.com/epfl-lara/rust-stainless/issues/103
(As always, there's a preliminary clean-up commit, which can/may be reviewed separately.)
PhantomData is just a field-less marker, so it is safe to extract it as a field-less ADT. The trick used here, is that we detect the
and extract it as
Closes #69.
The awesome thing is, that the existing
extract_adtfunction also works for crate-external ADTs. (Therefore, the feature addition in the last commit of this PR is minimal effort.) This opens the door to using the realstd::*::Option/Result/etc. Tracking that feature here: https://github.com/epfl-lara/rust-stainless/issues/103(As always, there's a preliminary clean-up commit, which can/may be reviewed separately.)