Lean.Expr construction helpers bound to a loaded LeanLibrary.
| 13 | |
| 14 | |
| 15 | class ExprBuilder: |
| 16 | """Lean.Expr construction helpers bound to a loaded LeanLibrary.""" |
| 17 | |
| 18 | def __init__(self, lib): |
| 19 | self.Name = lib.Name |
| 20 | self.Expr = lib.Expr |
| 21 | self.Level = lib.Level |
| 22 | self.Literal = lib.Literal |
| 23 | self.BinderInfo = lib.BinderInfo |
| 24 | self._z = self.Level.zero |
| 25 | |
| 26 | # -- Name helpers --------------------------------------------------------- |
| 27 | |
| 28 | def mk_name(self, s: str): |
| 29 | """``"HAdd.hAdd"`` -> nested ``Name.str``.""" |
| 30 | n = self.Name.anonymous |
| 31 | for part in s.split("."): |
| 32 | n = self.Name.str(n, part) |
| 33 | return n |
| 34 | |
| 35 | # -- Core Expr builders --------------------------------------------------- |
| 36 | |
| 37 | def mk_const(self, name: str, levels=None): |
| 38 | return self.Expr.const(self.mk_name(name), levels or []) |
| 39 | |
| 40 | def mk_app(self, fn, arg): |
| 41 | return self.Expr.app(fn, arg) |
| 42 | |
| 43 | def mk_apps(self, fn, *args): |
| 44 | e = fn |
| 45 | for a in args: |
| 46 | e = self.Expr.app(e, a) |
| 47 | return e |
| 48 | |
| 49 | def mk_bvar(self, idx: int): |
| 50 | return self.Expr.bvar(idx) |
| 51 | |
| 52 | def mk_forall(self, name: str, ty, body, binder_info=None): |
| 53 | bi = binder_info if binder_info is not None else self.BinderInfo.default |
| 54 | return self.Expr.forallE(self.mk_name(name), ty, body, bi) |
| 55 | |
| 56 | def mk_nat_lit(self, n: int): |
| 57 | return self.Expr.lit(self.Literal.natVal(n)) |
| 58 | |
| 59 | def mk_sort(self, level): |
| 60 | return self.Expr.sort(level) |
| 61 | |
| 62 | # -- Int-specific helpers ------------------------------------------------- |
| 63 | |
| 64 | @property |
| 65 | def INT(self): |
| 66 | return self.mk_const("Int") |
| 67 | |
| 68 | def mk_int(self, n: int): |
| 69 | if n >= 0: |
| 70 | return self.mk_apps(self.mk_const("Int.ofNat"), self.mk_nat_lit(n)) |
| 71 | else: |
| 72 | return self.mk_apps(self.mk_const("Int.negSucc"), self.mk_nat_lit(-n - 1)) |