Convert a Python ASTSort to a Lean Z3Sort value.
(lib: Any, sort: ASTSort)
| 172 | |
| 173 | |
| 174 | def _marshal_sort(lib: Any, sort: ASTSort) -> Any: |
| 175 | """Convert a Python ASTSort to a Lean Z3Sort value.""" |
| 176 | Z3Sort = lib.Z3Sort |
| 177 | if isinstance(sort, PropSort): |
| 178 | return Z3Sort.prop |
| 179 | if isinstance(sort, IntASTSort): |
| 180 | return Z3Sort.int |
| 181 | if isinstance(sort, NatASTSort): |
| 182 | return Z3Sort.nat |
| 183 | if isinstance(sort, RealASTSort): |
| 184 | return Z3Sort.real |
| 185 | if isinstance(sort, TypeASTSort): |
| 186 | return Z3Sort.type |
| 187 | if isinstance(sort, StringASTSort): |
| 188 | return Z3Sort.string |
| 189 | if isinstance(sort, BitvecASTSort): |
| 190 | return Z3Sort.bitvec(sort.width) |
| 191 | if isinstance(sort, UninterpASTSort): |
| 192 | return Z3Sort.uninterp(sort.name) |
| 193 | if isinstance(sort, FpASTSort): |
| 194 | return Z3Sort.fp(sort.ebits, sort.sbits) |
| 195 | if isinstance(sort, FinDomainASTSort): |
| 196 | return Z3Sort.finDomain(sort.size) |
| 197 | if isinstance(sort, ArrowASTSort): |
| 198 | dom = _marshal_sort(lib, sort.dom) |
| 199 | cod = _marshal_sort(lib, sort.cod) |
| 200 | return Z3Sort.arrow(dom, cod) |
| 201 | if isinstance(sort, InductiveASTSort): |
| 202 | return Z3Sort.inductive_(sort.name) |
| 203 | if isinstance(sort, CharASTSort): |
| 204 | return Z3Sort.char |
| 205 | if isinstance(sort, SeqASTSort): |
| 206 | elem = _marshal_sort(lib, sort.elem) |
| 207 | return Z3Sort.seq(elem) |
| 208 | raise TypeError(f"Unknown ASTSort: {type(sort)}") |
| 209 | |
| 210 | |
| 211 | def _marshal_binop(lib: Any, op: str) -> Any: |
no outgoing calls
no test coverage detected