WIP: Add support for partial orders

creusot-contracts-proc/src/pretyping.rs

@@ -59,16 +59,16 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
                     Ok(quote_spanned! {sp=> ::creusot_contracts::__stubs::neq(#left, #right) })
                 }
                 Lt(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::lt_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::lt_log(#left, #right) },
                 ),
                 Le(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::le_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::le_log(#left, #right) },
                 ),
                 Ge(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::ge_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::ge_log(#left, #right) },
                 ),
                 Gt(_) => Ok(
-                    quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::gt_log(#left, #right) },
+                    quote_spanned! {sp=> ::creusot_contracts::logic::PartialOrdLogic::gt_log(#left, #right) },
                 ),
                 _ => Ok(quote_spanned! {sp=> #left #op #right }),
             }

creusot-contracts/src/lib.rs

@@ -175,7 +175,7 @@ pub mod well_founded;
 // We add some common things at the root of the creusot-contracts library
 pub use crate::{
     ghost::Ghost,
-    logic::{Int, OrdLogic, Seq},
+    logic::{Int, PartialOrdLogic, OrdLogic, Seq},
     macros::*,
     model::{DeepModel, ShallowModel},
     resolve::Resolve,

creusot-contracts/src/logic.rs

@@ -14,6 +14,6 @@ pub use fset::FSet;
 pub use int::Int;
 pub use mapping::Mapping;
 pub use ops::IndexLogic;
-pub use ord::OrdLogic;
+pub use ord::{PartialOrdLogic, OrdLogic};
 pub use seq::Seq;
 pub use set::Set;