Convert an effectful Term to a Lean proposition string.
(vc_term, var_names, var_ops, precond_terms)
| 83 | |
| 84 | |
| 85 | def _build_lean_str(vc_term, var_names, var_ops, precond_terms) -> str: |
| 86 | """Convert an effectful Term to a Lean proposition string.""" |
| 87 | int_ops = defdata.dispatch(int) |
| 88 | |
| 89 | def _wrap(x): |
| 90 | s = str(x) if isinstance(x, int) else x |
| 91 | if isinstance(x, int) and x < 0: |
| 92 | return f"({s})" |
| 93 | return s |
| 94 | |
| 95 | str_handler = {} |
| 96 | for name in var_names: |
| 97 | str_handler[var_ops[name]] = (lambda n: lambda: n)(name) |
| 98 | |
| 99 | str_handler[int_ops.__add__] = lambda a, b: f"({_wrap(a)} + {_wrap(b)})" |
| 100 | str_handler[int_ops.__sub__] = lambda a, b: f"({_wrap(a)} - {_wrap(b)})" |
| 101 | str_handler[int_ops.__mul__] = lambda a, b: f"({_wrap(a)} * {_wrap(b)})" |
| 102 | str_handler[int_ops.__gt__] = lambda a, b: f"({_wrap(a)} > {_wrap(b)})" |
| 103 | str_handler[int_ops.__ge__] = lambda a, b: f"({_wrap(a)} >= {_wrap(b)})" |
| 104 | str_handler[int_ops.__lt__] = lambda a, b: f"({_wrap(a)} < {_wrap(b)})" |
| 105 | str_handler[int_ops.__le__] = lambda a, b: f"({_wrap(a)} <= {_wrap(b)})" |
| 106 | |
| 107 | with handler(str_handler): |
| 108 | body_str = evaluate(vc_term) |
| 109 | prec_strs = [evaluate(p) for p in precond_terms] |
| 110 | |
| 111 | quant = " ".join(f"({n} : Int)" for n in var_names) |
| 112 | if prec_strs: |
| 113 | precs = " → ".join(prec_strs) |
| 114 | return f"∀ {quant}, {precs} → {body_str}" |
| 115 | return f"∀ {quant}, {body_str}" |
| 116 | |
| 117 | |
| 118 | # --------------------------------------------------------------------------- |
no test coverage detected