Skip to content

Commit d6cec33

Browse files
petros-markopetros-marko
authored
Translate Flux Bool to Prop in Lean and open Classical everywhere (#1527)
* Translate Flux bool to Prop in Lean and open Classical everywhere * Less noncomputable stuff
1 parent beaebe5 commit d6cec33

File tree

2 files changed

+19
-46
lines changed

2 files changed

+19
-46
lines changed

‎crates/flux-infer/src/lean_encoding.rs‎

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,7 @@ use rustc_span::ErrorGuaranteed;
2525

2626
use crate::{
2727
fixpoint_encoding::{ConstDeps, InterpretedConst, KVarSolutions, SortDeps, fixpoint},
28-
lean_format::{
29-
self, BoolMode, LeanCtxt, WithLeanCtxt, def_id_to_pascal_case, snake_case_to_pascal_case,
30-
},
28+
lean_format::{self, LeanCtxt, WithLeanCtxt, def_id_to_pascal_case, snake_case_to_pascal_case},
3129
};
3230

3331
/// Helper macro to create Vec<String> from string-like values
@@ -290,7 +288,6 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
290288
adt_map: &self.sort_deps.adt_map,
291289
opaque_adt_map: &self.sort_deps.opaque_sorts,
292290
kvar_solutions: &self.kvar_solutions,
293-
bool_mode: BoolMode::Bool,
294291
}
295292
}
296293

@@ -314,6 +311,10 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
314311
snake_case_to_pascal_case(&name)
315312
}
316313

314+
fn open_classical(&self) -> &str {
315+
"open Classical"
316+
}
317+
317318
fn new(
318319
genv: GlobalEnv<'genv, 'tcx>,
319320
def_id: MaybeExternId,
@@ -416,6 +417,7 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
416417
let path = file.path(self.genv);
417418
if let Some(mut file) = create_file_with_dirs(path)? {
418419
writeln!(file, "{}", &LeanFile::Fluxlib.import(self.genv))?;
420+
writeln!(file, "{}", self.open_classical())?;
419421
namespaced(&mut file, |f| {
420422
writeln!(f, "def {} := sorry", WithLeanCtxt { item: sort, cx: &self.lean_cx() })
421423
})?;
@@ -456,6 +458,7 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
456458
for dep in self.data_decl_dependencies(data_decl) {
457459
writeln!(file, "{}", dep.import(self.genv))?;
458460
}
461+
writeln!(file, "{}", self.open_classical())?;
459462

460463
// write data decl
461464
namespaced(&mut file, |f| {
@@ -527,6 +530,7 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
527530
for dep in self.fun_def_dependencies(did, fun_def) {
528531
writeln!(file, "{}", dep.import(self.genv))?;
529532
}
533+
writeln!(file, "{}", self.open_classical())?;
530534

531535
// write fun def
532536
namespaced(&mut file, |f| {
@@ -555,6 +559,8 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
555559
writeln!(file, "{}", self.sort_file(&dep).import(self.genv))?;
556560
}
557561

562+
writeln!(file, "{}", self.open_classical())?;
563+
558564
namespaced(&mut file, |f| {
559565
if let Some(comment) = &const_decl.comment {
560566
writeln!(f, "--{comment}")?;
@@ -683,6 +689,7 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
683689
let path = LeanFile::Vc(def_id).path(self.genv);
684690
if let Some(mut file) = create_file_with_dirs(path)? {
685691
self.generate_vc_imports(&mut file)?;
692+
writeln!(file, "{}", self.open_classical())?;
686693

687694
let vc_name = vc_name(self.genv, def_id);
688695
// 3. Write the VC
@@ -715,6 +722,7 @@ impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx> {
715722
if let Some(mut file) = create_file_with_dirs(path)? {
716723
writeln!(file, "{}", LeanFile::Fluxlib.import(self.genv))?;
717724
writeln!(file, "{}", LeanFile::Vc(def_id).import(self.genv))?;
725+
writeln!(file, "{}", self.open_classical())?;
718726
namespaced(&mut file, |f| {
719727
writeln!(f, "def {proof_name} : {vc_name} := by")?;
720728
writeln!(f, " unfold {vc_name}")?;

‎crates/flux-infer/src/lean_format.rs‎

Lines changed: 7 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -23,25 +23,12 @@ use crate::fixpoint_encoding::{
2323
},
2424
};
2525

26-
#[derive(Debug, Clone, Copy)]
27-
pub enum BoolMode {
28-
Bool,
29-
Prop,
30-
}
31-
3226
pub struct LeanCtxt<'a, 'genv, 'tcx> {
3327
pub genv: GlobalEnv<'genv, 'tcx>,
3428
pub pretty_var_map: &'a PrettyMap<LocalVar>,
3529
pub adt_map: &'a FxIndexSet<DefId>,
3630
pub opaque_adt_map: &'a [(FluxDefId, SortDecl)],
3731
pub kvar_solutions: &'a KVarSolutions,
38-
pub bool_mode: BoolMode,
39-
}
40-
41-
impl<'a, 'genv, 'tcx> LeanCtxt<'a, 'genv, 'tcx> {
42-
pub(crate) fn with_bool_mode(&self, bool_mode: BoolMode) -> Self {
43-
LeanCtxt { bool_mode, ..*self }
44-
}
4532
}
4633

4734
pub struct WithLeanCtxt<'a, 'b, 'genv, 'tcx, T> {
@@ -320,12 +307,7 @@ impl LeanFmt for Sort {
320307
fn lean_fmt(&self, f: &mut std::fmt::Formatter, cx: &LeanCtxt) -> std::fmt::Result {
321308
match self {
322309
Sort::Int => write!(f, "Int"),
323-
Sort::Bool => {
324-
match cx.bool_mode {
325-
BoolMode::Bool => write!(f, "Bool"),
326-
BoolMode::Prop => write!(f, "Prop"),
327-
}
328-
}
310+
Sort::Bool => write!(f, "Prop"),
329311
Sort::Real => write!(f, "Real"),
330312
Sort::Str => write!(f, "String"),
331313
Sort::Func(f_sort) => {
@@ -394,12 +376,7 @@ impl LeanFmt for Expr {
394376
Expr::Constant(c) => {
395377
match c {
396378
Constant::Numeral(n) => write!(f, "{n}",),
397-
Constant::Boolean(b) => {
398-
match cx.bool_mode {
399-
BoolMode::Bool => write!(f, "{}", if *b { "true" } else { "false" }),
400-
BoolMode::Prop => write!(f, "{}", if *b { "True" } else { "False" }),
401-
}
402-
}
379+
Constant::Boolean(b) => write!(f, "{}", if *b { "True" } else { "False" }),
403380
Constant::String(s) => write!(f, "{}", s.display()),
404381
Constant::Real(n) => write!(f, "{n}.0"),
405382
Constant::BitVec(bv, size) => write!(f, "{}#{}", bv, size),
@@ -452,8 +429,7 @@ impl LeanFmt for Expr {
452429
write!(f, ")")?;
453430
if let Some(out_sort) = out_sort {
454431
write!(f, " : (")?;
455-
let sort_cx = cx.with_bool_mode(BoolMode::Bool);
456-
out_sort.lean_fmt(f, &sort_cx)?;
432+
out_sort.lean_fmt(f, &cx)?;
457433
write!(f, "))")?;
458434
}
459435
Ok(())
@@ -462,10 +438,7 @@ impl LeanFmt for Expr {
462438
write!(f, "(")?;
463439
for (i, expr) in exprs.iter().enumerate() {
464440
if i > 0 {
465-
match cx.bool_mode {
466-
BoolMode::Bool => write!(f, " && ")?,
467-
BoolMode::Prop => write!(f, " ∧ ")?,
468-
};
441+
write!(f, " ∧ ")?;
469442
}
470443
expr.lean_fmt(f, cx)?;
471444
}
@@ -475,10 +448,7 @@ impl LeanFmt for Expr {
475448
write!(f, "(")?;
476449
for (i, expr) in exprs.iter().enumerate() {
477450
if i > 0 {
478-
match cx.bool_mode {
479-
BoolMode::Bool => write!(f, " || ")?,
480-
BoolMode::Prop => write!(f, " ∨ ")?,
481-
};
451+
write!(f, " ∨ ")?;
482452
}
483453
expr.lean_fmt(f, cx)?;
484454
}
@@ -501,10 +471,7 @@ impl LeanFmt for Expr {
501471
}
502472
Expr::Not(inner) => {
503473
write!(f, "(")?;
504-
match cx.bool_mode {
505-
BoolMode::Bool => write!(f, "!")?,
506-
BoolMode::Prop => write!(f, "¬")?,
507-
};
474+
write!(f, "¬")?;
508475
inner.as_ref().lean_fmt(f, cx)?;
509476
write!(f, ")")
510477
}
@@ -559,7 +526,7 @@ impl LeanFmt for Expr {
559526
impl LeanFmt for FunDef {
560527
fn lean_fmt(&self, f: &mut fmt::Formatter, cx: &LeanCtxt) -> fmt::Result {
561528
let FunDef { name, sort, comment: _, body } = self;
562-
write!(f, "def ")?;
529+
write!(f, "noncomputable def ")?;
563530
name.lean_fmt(f, cx)?;
564531
if let Some(body) = body {
565532
for (arg, arg_sort) in iter::zip(&body.args, &sort.inputs) {
@@ -675,8 +642,6 @@ impl<'a> LeanFmt for LeanKConstraint<'a> {
675642
if !cx.kvar_solutions.is_empty() {
676643
writeln!(f, "namespace {namespace}\n")?;
677644

678-
let cx = cx.with_bool_mode(BoolMode::Prop);
679-
680645
if !cx.kvar_solutions.cut_solutions.is_empty() {
681646
writeln!(f, "-- cyclic (cut) kvars")?;
682647
for kvar_solution in &cx.kvar_solutions.cut_solutions {

0 commit comments

Comments
 (0)