kdrag.printers.lean

Functions

accessor_def(dt, n, i)	Make a lean definition that matches accessor, otherwise returns default.
decl_axiom(f)	Convert a function declaration to a Lean axiom definition.
decl_sig(f)	Convert a function declaration to a Lean signature.
of_datatype(dt)	Convert a datatype to a Lean inductive type definition.
of_expr(e)
of_sort(s)	Convert a sort to a Lean type.
run_lean(filename)
sort_axiom(s)	Convert uninterpreted sort to a Lean axiom definition.

kdrag.printers.lean.accessor_def(dt: DatatypeSortRef, n: int, i: int) → str

Make a lean definition that matches accessor, otherwise returns default. This might not be a perfect translation of accessor behavior in SMTLIB

Parameters:

• dt (DatatypeSortRef)

• n (int)

• i (int)

Return type:

str

kdrag.printers.lean.decl_axiom(f: FuncDeclRef) → str

Convert a function declaration to a Lean axiom definition.

>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> decl_axiom(f)
'axiom f : Int -> Int -> Bool\n'

Parameters:

f (FuncDeclRef)

Return type:

str

kdrag.printers.lean.decl_sig(f: FuncDeclRef) → str

Convert a function declaration to a Lean signature.

>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> decl_sig(f)
'f : Int -> Int -> Bool'

Parameters:

f (FuncDeclRef)

Return type:

str

kdrag.printers.lean.of_datatype(dt: DatatypeSortRef) → str

Convert a datatype to a Lean inductive type definition.

>>> Nat = smt.Datatype("Nat")
>>> Nat.declare("Zero")
>>> Nat.declare("Succ", ("pred", Nat))
>>> Nat = Nat.create()
>>> of_datatype(Nat)
'inductive Nat : Type where\n| Zero : Nat\n| Succ : Nat -> Nat\nderiving BEq, Inhabited, Repr, DecidableEq\n'

Parameters:

dt (DatatypeSortRef)

Return type:

str

kdrag.printers.lean.of_expr(e: ExprRef)

>>> x,y,z = smt.Ints("x y z")
>>> of_expr(x)
'(x : Int)'
>>> of_expr(x + y + z)
'(((x : Int) + (y : Int)) + (z : Int))'
>>> of_expr(smt.If(x == x, y, z))
'(if ((x : Int) = (x : Int)) then (y : Int) else (z : Int))'

Parameters:

e (ExprRef)

kdrag.printers.lean.of_sort(s: SortRef) → str

Convert a sort to a Lean type.

>>> of_sort(smt.BoolSort())
'Bool'
>>> of_sort(smt.BitVecSort(8))
'(BitVec 8)'
>>> of_sort(smt.ArraySort(smt.BitVecSort(8), smt.BitVecSort(16)))
'((BitVec 8) -> (BitVec 16))'

Parameters:

s (SortRef)

Return type:

str

kdrag.printers.lean.run_lean(filename: str)

Parameters:

filename (str)

kdrag.printers.lean.sort_axiom(s: SortRef) → str

Convert uninterpreted sort to a Lean axiom definition.

Parameters:

s (SortRef)

Return type:

str