1use core::fmt;
2
3use itertools::Itertools;
4use liquid_fixpoint::{FixpointFmt, Identifier, ThyFunc};
5
6use crate::{
7 fixpoint_encoding::fixpoint::{
8 BinOp, BinRel, ConstDecl, Constant, Constraint, Expr, FunDef, Pred, Sort, Var,
9 },
10 lean_encoding::{ConstDef, LeanEncoder},
11};
12
13struct LeanSort<'a>(&'a Sort);
14struct LeanFunDef<'a>(&'a FunDef);
15struct LeanConstDef<'a>(&'a ConstDef);
16struct LeanConstraint<'a>(&'a Constraint);
17struct LeanPred<'a>(&'a Pred);
18struct LeanExpr<'a>(&'a Expr);
19struct LeanVar<'a>(&'a Var);
20struct LeanThyFunc<'a>(&'a ThyFunc);
21
22impl<'a> fmt::Display for LeanThyFunc<'a> {
23 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
24 match self.0 {
25 ThyFunc::IntToBv8 => write!(f, "BitVec.ofInt 8"),
26 ThyFunc::IntToBv32 => write!(f, "BitVec.ofInt 32"),
27 ThyFunc::IntToBv64 => write!(f, "BitVec.ofInt 64"),
28 ThyFunc::Bv8ToInt | ThyFunc::Bv32ToInt | ThyFunc::Bv64ToInt => {
29 write!(f, "BitVec.toNat")
30 }
31 ThyFunc::BvAdd => write!(f, "BitVec.add"),
32 ThyFunc::BvSub => write!(f, "BitVec.sub"),
33 ThyFunc::BvMul => write!(f, "BitVec.mul"),
34 ThyFunc::BvNeg => write!(f, "BitVec.neg"),
35 ThyFunc::BvSdiv => write!(f, "BitVec.sdiv"),
36 ThyFunc::BvSrem => write!(f, "BitVec.srem"),
37 ThyFunc::BvUdiv => write!(f, "BitVec.udiv"),
38 ThyFunc::BvAnd => write!(f, "BitVec.and"),
39 ThyFunc::BvOr => write!(f, "BitVec.or"),
40 ThyFunc::BvXor => write!(f, "BitVec.xor"),
41 ThyFunc::BvNot => write!(f, "BitVec.not"),
42 ThyFunc::BvSle => write!(f, "BitVec.sle"),
43 ThyFunc::BvSlt => write!(f, "BitVec.slt"),
44 ThyFunc::BvUle => write!(f, "BitVec.ule"),
45 ThyFunc::BvUlt => write!(f, "BitVec.ult"),
46 ThyFunc::BvAshr => write!(f, "BitVec.sshiftRight"),
47 ThyFunc::BvLshr => write!(f, "BitVec.ushiftRight"),
48 ThyFunc::BvShl => write!(f, "BitVec.shiftLeft"),
49 ThyFunc::BvSignExtend(size) => write!(f, "BitVec.signExtend {}", size),
50 ThyFunc::BvZeroExtend(size) => write!(f, "BitVec.zeroExtend {}", size),
51 ThyFunc::BvUrem | ThyFunc::BvSge | ThyFunc::BvSgt | ThyFunc::BvUge | ThyFunc::BvUgt => {
52 todo!("No builtin {}, define a local function {} and call it here", self.0, self.0)
53 }
54 func => panic!("Unsupported theory function {}", func),
55 }
56 }
57}
58
59impl<'a> fmt::Display for LeanVar<'a> {
60 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
61 write!(f, "{}", self.0.display().to_string().replace("$", "_"))
62 }
63}
64
65impl<'a> fmt::Display for LeanConstDef<'a> {
66 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
67 let LeanConstDef(ConstDef(ConstDecl { name, sort, comment: _ }, def)) = self;
68 if let Some(def) = def {
69 write!(f, "def {} : {} := {}", LeanVar(name), LeanSort(sort), LeanExpr(def))
70 } else {
71 write!(f, "axiom {} : {}", LeanVar(name), LeanSort(sort))
72 }
73 }
74}
75
76impl<'a> fmt::Display for LeanSort<'a> {
77 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
78 match self.0 {
79 Sort::Int => write!(f, "Int"),
80 Sort::Bool => write!(f, "Bool"),
81 Sort::Real => write!(f, "Real"),
82 Sort::Str => write!(f, "String"),
83 Sort::Func(f_sort) => {
84 write!(f, "({} -> {})", LeanSort(&f_sort[0]), LeanSort(&f_sort[1]))
85 }
86 _ => todo!(),
87 }
88 }
89}
90
91impl<'a> fmt::Display for LeanExpr<'a> {
92 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
93 match self.0 {
94 Expr::Var(v) => write!(f, "{}", LeanVar(v)),
95 Expr::Constant(c) => {
96 match c {
97 Constant::Numeral(n) => write!(f, "{}", n),
98 Constant::Boolean(b) => write!(f, "{}", b),
99 Constant::String(s) => write!(f, "{}", s.display()),
100 Constant::Decimal(d) => write!(f, "{}", d.display()),
101 Constant::BitVec(bv, size) => write!(f, "{}#{}", bv, size),
102 }
103 }
104 Expr::BinaryOp(bin_op, args) => {
105 let bin_op_str = match bin_op {
106 BinOp::Add => "+",
107 BinOp::Sub => "-",
108 BinOp::Mul => "*",
109 BinOp::Div => "/",
110 BinOp::Mod => "%",
111 };
112 write!(f, "({} {} {})", LeanExpr(&args[0]), bin_op_str, LeanExpr(&args[1]))
113 }
114 Expr::Atom(bin_rel, args) => {
115 let bin_rel_str = match bin_rel {
116 BinRel::Eq => "=",
117 BinRel::Ne => "≠",
118 BinRel::Le => "≤",
119 BinRel::Lt => "<",
120 BinRel::Ge => "≥",
121 BinRel::Gt => ">",
122 };
123 write!(f, "({} {} {})", LeanExpr(&args[0]), bin_rel_str, LeanExpr(&args[1]))
124 }
125 Expr::App(function, args) => {
126 write!(
127 f,
128 "({} {})",
129 LeanExpr(function.as_ref()),
130 args.iter().map(LeanExpr).format(" ")
131 )
132 }
133 Expr::And(exprs) => {
134 write!(f, "({})", exprs.iter().map(LeanExpr).format(" && "))
135 }
136 Expr::Or(exprs) => {
137 write!(f, "({})", exprs.iter().map(LeanExpr).format(" || "))
138 }
139 Expr::Neg(inner) => {
140 write!(f, "(-{})", LeanExpr(inner.as_ref()))
141 }
142 Expr::IfThenElse(ite) => {
143 let [condition, if_true, if_false] = ite.as_ref();
144 write!(
145 f,
146 "(if {} then {} else {})",
147 LeanExpr(condition),
148 LeanExpr(if_true),
149 LeanExpr(if_false)
150 )
151 }
152 Expr::Not(inner) => {
153 write!(f, "(¬{})", LeanExpr(inner.as_ref()))
154 }
155 Expr::Imp(implication) => {
156 let [lhs, rhs] = implication.as_ref();
157 write!(f, "({} -> {})", LeanExpr(lhs), LeanExpr(rhs))
158 }
159 Expr::Iff(equiv) => {
160 let [lhs, rhs] = equiv.as_ref();
161 write!(f, "({} <-> {})", LeanExpr(lhs), LeanExpr(rhs))
162 }
163 Expr::Let(binder, exprs) => {
164 let [def, body] = exprs.as_ref();
165 write!(f, "(let {} := {}; {})", LeanVar(binder), LeanExpr(def), LeanExpr(body))
166 }
167 Expr::ThyFunc(thy_func) => {
168 write!(f, "{}", LeanThyFunc(thy_func))
169 }
170 Expr::IsCtor(..) => {
171 todo!("not yet implemented: datatypes in lean")
172 }
173 }
174 }
175}
176
177impl<'a> fmt::Display for LeanFunDef<'a> {
178 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
179 let LeanFunDef(FunDef { name, args, out, comment: _, body }) = self;
180 writeln!(
181 f,
182 "def {} {} : {} :=",
183 LeanVar(name),
184 args.iter()
185 .map(|(arg, arg_sort)| format!("({} : {})", LeanVar(arg), LeanSort(arg_sort)))
186 .collect::<Vec<_>>()
187 .join(" "),
188 LeanSort(out)
189 )?;
190 writeln!(f, " {}", LeanExpr(body))
191 }
192}
193
194impl<'a> fmt::Display for LeanPred<'a> {
195 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
196 match self.0 {
197 Pred::Expr(expr) => write!(f, "{}", LeanExpr(expr)),
198 Pred::And(preds) => write!(f, "({})", preds.iter().map(LeanPred).format(" ∧ ")),
199 Pred::KVar(_, _) => panic!("kvars should not appear when encoding in lean"),
200 }
201 }
202}
203
204impl<'a> fmt::Display for LeanConstraint<'a> {
205 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
206 match self.0 {
207 Constraint::ForAll(bind, inner) => {
208 if bind.pred.is_trivially_true() {
209 write!(
210 f,
211 "(∀ ({} : {}), {})",
212 LeanVar(&bind.name),
213 LeanSort(&bind.sort),
214 LeanConstraint(inner)
215 )
216 } else {
217 write!(
218 f,
219 "(∀ ({} : {}), ({} -> {}))",
220 LeanVar(&bind.name),
221 LeanSort(&bind.sort),
222 LeanPred(&bind.pred),
223 LeanConstraint(inner)
224 )
225 }
226 }
227 Constraint::Conj(constraints) => {
228 write!(f, "({})", constraints.iter().map(LeanConstraint).format(" ∧ "))
229 }
230 Constraint::Pred(pred, _) => {
231 write!(f, "{}", LeanPred(pred))
232 }
233 }
234 }
235}
236
237impl<'genv, 'tcx> fmt::Display for LeanEncoder<'genv, 'tcx> {
238 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
239 writeln!(f, "-- GENERATED; DO NOT EDIT --")?;
240 if !self.fun_defs().is_empty() {
241 writeln!(f, "-- FUNCTIONS --")?;
242 for fun_def in self.fun_defs() {
243 writeln!(f, "{}", LeanFunDef(fun_def))?;
244 }
245 }
246 if !self.constants().is_empty() {
247 writeln!(f, "-- Constants --")?;
248 for const_def in self.constants() {
249 writeln!(f, "{}", LeanConstDef(const_def))?;
250 }
251 }
252 writeln!(f, "-- THEOREM --")?;
253 writeln!(
254 f,
255 "def {} : Prop := {}",
256 self.theorem_name().replace(".", "_"),
257 LeanConstraint(self.constraint())
258 )
259 }
260}