1use core::fmt;
2
3use flux_middle::global_env::GlobalEnv;
4use itertools::Itertools;
5use liquid_fixpoint::{FixpointFmt, Identifier, ThyFunc};
6
7use crate::fixpoint_encoding::fixpoint::{
8 BinOp, BinRel, ConstDecl, Constant, Constraint, DataDecl, DataField, DataSort, Expr, FunDef,
9 KVarDecl, Pred, Sort, SortCtor, SortDecl, Var,
10};
11
12struct LeanSort<'a>(&'a Sort);
13struct LeanKVarDecl<'a>(&'a KVarDecl);
14pub struct LeanKConstraint<'a, 'genv, 'tcx>(
15 pub &'a [KVarDecl],
16 pub &'a Constraint,
17 pub GlobalEnv<'genv, 'tcx>,
18);
19pub struct LeanFunDef<'a, 'genv, 'tcx>(pub &'a FunDef, pub GlobalEnv<'genv, 'tcx>);
20pub struct LeanSortDecl<'a, 'genv, 'tcx>(pub &'a SortDecl, pub GlobalEnv<'genv, 'tcx>);
21pub struct LeanDataDecl<'a, 'genv, 'tcx>(pub &'a DataDecl, pub GlobalEnv<'genv, 'tcx>);
22pub struct LeanConstDecl<'a, 'genv, 'tcx>(pub &'a ConstDecl, pub GlobalEnv<'genv, 'tcx>);
23pub struct LeanSortVar<'a>(pub &'a DataSort);
24struct LeanDataField<'a>(&'a DataField);
25struct LeanConstraint<'a, 'genv, 'tcx>(&'a Constraint, GlobalEnv<'genv, 'tcx>);
26struct LeanPred<'a, 'genv, 'tcx>(&'a Pred, GlobalEnv<'genv, 'tcx>);
27struct LeanExpr<'a, 'genv, 'tcx>(&'a Expr, GlobalEnv<'genv, 'tcx>);
28pub struct LeanVar<'a, 'genv, 'tcx>(pub &'a Var, pub GlobalEnv<'genv, 'tcx>);
29struct LeanThyFunc<'a>(&'a ThyFunc);
30
31impl<'a, 'genv, 'tcx> fmt::Display for LeanSortDecl<'a, 'genv, 'tcx> {
32 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
33 write!(
34 f,
35 "{} {} : Type",
36 LeanSortVar(&self.0.name),
37 (0..(self.0.vars))
38 .map(|i| format!("(t{i} : Type) [Inhabited t{i}]"))
39 .format(" ")
40 )
41 }
42}
43
44impl<'a, 'genv, 'tcx> fmt::Display for LeanConstDecl<'a, 'genv, 'tcx> {
45 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
46 write!(f, "{} : {}", LeanVar(&self.0.name, self.1), LeanSort(&self.0.sort))
47 }
48}
49
50impl<'a> fmt::Display for LeanDataField<'a> {
51 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
52 write!(
53 f,
54 "({} : {})",
55 self.0.name.display().to_string().replace("$", "_"),
56 LeanSort(&self.0.sort)
57 )
58 }
59}
60
61impl<'a> fmt::Display for LeanSortVar<'a> {
62 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
63 match self.0 {
64 DataSort::User(def_id) => write!(f, "{}", def_id.name()),
65 _ => write!(f, "{}", self.0.display().to_string().replace("$", "_")),
66 }
67 }
68}
69
70impl<'a, 'genv, 'tcx> fmt::Display for LeanDataDecl<'a, 'genv, 'tcx> {
71 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
72 if self.0.ctors.len() == 1 {
73 writeln!(
74 f,
75 "structure {} {} where",
76 LeanSortVar(&self.0.name),
77 (0..self.0.vars)
78 .map(|i| format!("(t{i} : Type) [Inhabited t{i}]"))
79 .format(" ")
80 )?;
81 writeln!(f, " {}::", self.0.ctors[0].name.display().to_string().replace("$", "_"),)?;
82 for field in &self.0.ctors[0].fields {
83 writeln!(f, " {}", LeanDataField(field))?;
84 }
85 } else {
86 writeln!(
87 f,
88 "inductive {} {} where",
89 LeanSortVar(&self.0.name),
90 (0..self.0.vars)
91 .map(|i| format!("(t{i} : Type) [Inhabited t{i}]"))
92 .format(" ")
93 )?;
94 for data_ctor in &self.0.ctors {
95 writeln!(
96 f,
97 "| {} {}",
98 LeanVar(&data_ctor.name, self.1),
99 data_ctor.fields.iter().map(LeanDataField).format(" ")
100 )?;
101 }
102 }
103 Ok(())
104 }
105}
106
107impl<'a> fmt::Display for LeanThyFunc<'a> {
108 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
109 match self.0 {
110 ThyFunc::IntToBv8 => write!(f, "BitVec.ofInt 8"),
111 ThyFunc::IntToBv32 => write!(f, "BitVec.ofInt 32"),
112 ThyFunc::IntToBv64 => write!(f, "BitVec.ofInt 64"),
113 ThyFunc::Bv8ToInt | ThyFunc::Bv32ToInt | ThyFunc::Bv64ToInt => {
114 write!(f, "BitVec.toNat")
115 }
116 ThyFunc::BvAdd => write!(f, "BitVec.add"),
117 ThyFunc::BvSub => write!(f, "BitVec.sub"),
118 ThyFunc::BvMul => write!(f, "BitVec.mul"),
119 ThyFunc::BvNeg => write!(f, "BitVec.neg"),
120 ThyFunc::BvSdiv => write!(f, "BitVec.sdiv"),
121 ThyFunc::BvSrem => write!(f, "BitVec.srem"),
122 ThyFunc::BvUdiv => write!(f, "BitVec.udiv"),
123 ThyFunc::BvAnd => write!(f, "BitVec.and"),
124 ThyFunc::BvOr => write!(f, "BitVec.or"),
125 ThyFunc::BvXor => write!(f, "BitVec.xor"),
126 ThyFunc::BvNot => write!(f, "BitVec.not"),
127 ThyFunc::BvSle => write!(f, "BitVec.sle"),
128 ThyFunc::BvSlt => write!(f, "BitVec.slt"),
129 ThyFunc::BvUle => write!(f, "BitVec.ule"),
130 ThyFunc::BvUlt => write!(f, "BitVec.ult"),
131 ThyFunc::BvAshr => write!(f, "BitVec_sshiftRight"),
132 ThyFunc::BvLshr => write!(f, "BitVec_ushiftRight"),
133 ThyFunc::BvShl => write!(f, "BitVec_shiftLeft"),
134 ThyFunc::BvSignExtend(size) => write!(f, "BitVec.signExtend {}", size),
135 ThyFunc::BvZeroExtend(size) => write!(f, "BitVec.zeroExtend {}", size),
136 ThyFunc::BvUrem => write!(f, "BitVec.umod"),
137 ThyFunc::BvSge => write!(f, "BitVec_sge"),
138 ThyFunc::BvSgt => write!(f, "BitVec_sgt"),
139 ThyFunc::BvUge => write!(f, "BitVec_uge"),
140 ThyFunc::BvUgt => write!(f, "BitVec_ugt"),
141 ThyFunc::MapDefault => write!(f, "SmtMap_default"),
142 ThyFunc::MapSelect => write!(f, "SmtMap_select"),
143 ThyFunc::MapStore => write!(f, "SmtMap_store"),
144 func => panic!("Unsupported theory function {}", func),
145 }
146 }
147}
148
149impl<'a, 'genv, 'tcx> fmt::Display for LeanVar<'a, 'genv, 'tcx> {
150 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
151 match self.0 {
152 Var::Global(_gvar, Some(def_id)) => {
153 let path = self
154 .1
155 .tcx()
156 .def_path(def_id.parent())
157 .to_filename_friendly_no_crate()
158 .replace("-", "_");
159 if path.is_empty() {
160 write!(f, "{}", def_id.name())
161 } else {
162 write!(f, "{path}_{}", def_id.name())
163 }
164 }
165 Var::DataCtor(adt_id, _) | Var::DataProj { adt_id, field: _ } => {
166 write!(
167 f,
168 "{}.{}",
169 LeanSortVar(&DataSort::Adt(*adt_id)),
170 self.0.display().to_string().replace("$", "_")
171 )
172 }
173 _ => {
174 write!(f, "{}", self.0.display().to_string().replace("$", "_"))
175 }
176 }
177 }
178}
179
180impl<'a> fmt::Display for LeanSort<'a> {
181 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
182 match self.0 {
183 Sort::Int => write!(f, "Int"),
184 Sort::Bool => write!(f, "Bool"),
185 Sort::Real => write!(f, "Real"),
186 Sort::Str => write!(f, "String"),
187 Sort::Func(f_sort) => {
188 write!(f, "({} -> {})", LeanSort(&f_sort[0]), LeanSort(&f_sort[1]))
189 }
190 Sort::App(sort_ctor, args) => {
191 match sort_ctor {
192 SortCtor::Data(sort) => {
193 if args.is_empty() {
194 write!(f, "{}", LeanSortVar(sort))
195 } else {
196 write!(
197 f,
198 "({} {})",
199 LeanSortVar(sort),
200 args.iter().map(LeanSort).format(" ")
201 )
202 }
203 }
204 SortCtor::Map => {
205 write!(f, "(SmtMap {} {})", LeanSort(&args[0]), LeanSort(&args[1]))
206 }
207 _ => todo!(),
208 }
209 }
210 Sort::BitVec(bv_size) => {
211 match bv_size.as_ref() {
212 Sort::BvSize(size) => write!(f, "BitVec {}", size),
213 s => panic!("encountered sort {} where bitvec size was expected", LeanSort(s)),
214 }
215 }
216 Sort::Abs(v, sort) => {
217 write!(f, "{{t{v} : Type}} -> [Inhabited t{v}] -> {}", LeanSort(sort.as_ref()))
218 }
219 Sort::Var(v) => write!(f, "t{v}"),
220 s => todo!("{:?}", s),
221 }
222 }
223}
224
225impl<'a, 'genv, 'tcx> fmt::Display for LeanExpr<'a, 'genv, 'tcx> {
226 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
227 match self.0 {
228 Expr::Var(v) => write!(f, "{}", LeanVar(v, self.1)),
229 Expr::Constant(c) => {
230 match c {
231 Constant::Numeral(n) => write!(f, "{n}",),
232 Constant::Boolean(b) => write!(f, "{b}"),
233 Constant::String(s) => write!(f, "{}", s.display()),
234 Constant::Real(n) => write!(f, "{n}.0"),
235 Constant::BitVec(bv, size) => write!(f, "{}#{}", bv, size),
236 }
237 }
238 Expr::BinaryOp(bin_op, args) => {
239 let bin_op_str = match bin_op {
240 BinOp::Add => "+",
241 BinOp::Sub => "-",
242 BinOp::Mul => "*",
243 BinOp::Div => "/",
244 BinOp::Mod => "%",
245 };
246 write!(
247 f,
248 "({} {} {})",
249 LeanExpr(&args[0], self.1),
250 bin_op_str,
251 LeanExpr(&args[1], self.1)
252 )
253 }
254 Expr::Atom(bin_rel, args) => {
255 let bin_rel_str = match bin_rel {
256 BinRel::Eq => "=",
257 BinRel::Ne => "≠",
258 BinRel::Le => "≤",
259 BinRel::Lt => "<",
260 BinRel::Ge => "≥",
261 BinRel::Gt => ">",
262 };
263 write!(
264 f,
265 "({} {} {})",
266 LeanExpr(&args[0], self.1),
267 bin_rel_str,
268 LeanExpr(&args[1], self.1)
269 )
270 }
271 Expr::App(function, args) => {
272 write!(
273 f,
274 "({} {})",
275 LeanExpr(function.as_ref(), self.1),
276 args.iter().map(|arg| LeanExpr(arg, self.1)).format(" ")
277 )
278 }
279 Expr::And(exprs) => {
280 write!(
281 f,
282 "({})",
283 exprs
284 .iter()
285 .map(|expr| LeanExpr(expr, self.1))
286 .format(" && ")
287 )
288 }
289 Expr::Or(exprs) => {
290 write!(
291 f,
292 "({})",
293 exprs
294 .iter()
295 .map(|expr| LeanExpr(expr, self.1))
296 .format(" || ")
297 )
298 }
299 Expr::Neg(inner) => {
300 write!(f, "(-{})", LeanExpr(inner.as_ref(), self.1))
301 }
302 Expr::IfThenElse(ite) => {
303 let [condition, if_true, if_false] = ite.as_ref();
304 write!(
305 f,
306 "(if {} then {} else {})",
307 LeanExpr(condition, self.1),
308 LeanExpr(if_true, self.1),
309 LeanExpr(if_false, self.1)
310 )
311 }
312 Expr::Not(inner) => {
313 write!(f, "(¬{})", LeanExpr(inner.as_ref(), self.1))
314 }
315 Expr::Imp(implication) => {
316 let [lhs, rhs] = implication.as_ref();
317 write!(f, "({} -> {})", LeanExpr(lhs, self.1), LeanExpr(rhs, self.1))
318 }
319 Expr::Iff(equiv) => {
320 let [lhs, rhs] = equiv.as_ref();
321 write!(f, "({} <-> {})", LeanExpr(lhs, self.1), LeanExpr(rhs, self.1))
322 }
323 Expr::Let(binder, exprs) => {
324 let [def, body] = exprs.as_ref();
325 write!(
326 f,
327 "(let {} := {}; {})",
328 LeanVar(binder, self.1),
329 LeanExpr(def, self.1),
330 LeanExpr(body, self.1)
331 )
332 }
333 Expr::ThyFunc(thy_func) => {
334 write!(f, "{}", LeanThyFunc(thy_func))
335 }
336 Expr::IsCtor(..) => {
337 todo!("not yet implemented: datatypes in lean")
338 }
339 Expr::Exists(..) => {
340 todo!("not yet implemented: exists in lean")
341 }
342 Expr::BoundVar(_) => {
343 unreachable!("bound vars should only be present in fixpoint output")
344 }
345 }
346 }
347}
348
349impl<'a, 'genv, 'tcx> fmt::Display for LeanFunDef<'a, 'genv, 'tcx> {
350 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
351 let LeanFunDef(FunDef { name, args, out, comment: _, body }, _) = self;
352 writeln!(
353 f,
354 "def {} {} : {} :=",
355 LeanVar(name, self.1),
356 args.iter()
357 .map(|(arg, arg_sort)| {
358 format!("({} : {})", LeanVar(arg, self.1), LeanSort(arg_sort))
359 })
360 .collect::<Vec<_>>()
361 .join(" "),
362 LeanSort(out)
363 )?;
364 writeln!(f, " {}", LeanExpr(body, self.1))
365 }
366}
367
368impl<'a, 'genv, 'tcx> fmt::Display for LeanPred<'a, 'genv, 'tcx> {
369 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
370 match self.0 {
371 Pred::Expr(expr) => write!(f, "{}", LeanExpr(expr, self.1)),
372 Pred::And(preds) => {
373 write!(
374 f,
375 "({})",
376 preds
377 .iter()
378 .map(|pred| LeanPred(pred, self.1))
379 .format(" ∧ ")
380 )
381 }
382 Pred::KVar(kvid, args) => {
383 write!(
384 f,
385 "({} {})",
386 kvid.display().to_string().replace("$", "_"),
387 args.iter().map(|var| LeanVar(var, self.1)).format(" ")
388 )
389 }
390 }
391 }
392}
393
394impl<'a> fmt::Display for LeanKVarDecl<'a> {
395 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
396 let sorts = self
397 .0
398 .sorts
399 .iter()
400 .enumerate()
401 .map(|(i, sort)| format!("(a{i} : {})", LeanSort(sort)))
402 .format(" -> ");
403 write!(f, "∃ {} : {} -> Prop", self.0.kvid.display().to_string().replace("$", "_"), sorts)
404 }
405}
406
407impl<'a, 'genv, 'tcx> fmt::Display for LeanKConstraint<'a, 'genv, 'tcx> {
408 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
409 if self.0.is_empty() {
410 write!(f, "{}", LeanConstraint(&self.1, self.2))
411 } else {
412 write!(
413 f,
414 "{}, {}",
415 self.0
416 .iter()
417 .map(|kvar_decl| LeanKVarDecl(&kvar_decl))
418 .format(", "),
419 LeanConstraint(&self.1, self.2)
420 )
421 }
422 }
423}
424
425impl<'a, 'genv, 'tcx> fmt::Display for LeanConstraint<'a, 'genv, 'tcx> {
426 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
427 match self.0 {
428 Constraint::ForAll(bind, inner) => {
429 if bind.pred.is_trivially_true() {
430 write!(
431 f,
432 "(∀ ({} : {}), {})",
433 LeanVar(&bind.name, self.1),
434 LeanSort(&bind.sort),
435 LeanConstraint(inner, self.1)
436 )
437 } else {
438 write!(
439 f,
440 "(∀ ({} : {}), ({} -> {}))",
441 LeanVar(&bind.name, self.1),
442 LeanSort(&bind.sort),
443 LeanPred(&bind.pred, self.1),
444 LeanConstraint(inner, self.1)
445 )
446 }
447 }
448 Constraint::Conj(constraints) => {
449 write!(
450 f,
451 "({})",
452 constraints
453 .iter()
454 .map(|constraint| LeanConstraint(constraint, self.1))
455 .format(" ∧ ")
456 )
457 }
458 Constraint::Pred(pred, _) => {
459 write!(f, "{}", LeanPred(pred, self.1))
460 }
461 }
462 }
463}