kdrag.parsers.microlean

A parser for a simple logical expression language using Lark. The syntax is inspired by Lean’s

Unicode symbols are not required, but if you like them, adding the Unicode LaTeX extension for VSCode https://marketplace.visualstudio.com/items?itemName=oijaz.unicode-latex Goto the File > Preferences > Settings of the plugin and add python to the enabled extensions. Reloading your window will enable access via backslash autocomplete commands. For example alpha will tab autocomplete to α.

Functions

`axiom`(tree, env)	Parse an axiom.
`binder`(tree, env)
`binders`(tree, env)
`define`(tree, env)	Parse a definition.
`expr`(tree, env)
`inductive`(s[, globals])	Parse an inductive datatype definition.
`inductive_of_tree`(tree[, globals])	Parse an inductive datatype definition.
`lean`(s[, globals])	Alias for parse to match Lean users' expectations.
`parse`(s[, globals])	Parse a logical expression into an SMT expression.
`quant`(vs, body_tree, q, env)
`sort`(tree, env)
`start`(tree, globals)
`theorem`(tree, env)	Parse a theorem.

Classes

Env(locals, globals)

class kdrag.parsers.microlean.Env(locals, globals)

Bases: NamedTuple

Parameters:

locals (dict)
globals (dict)

copy()

count(value, /): Return number of occurrences of value.

globals: dict: Alias for field number 1

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

locals: dict: Alias for field number 0

kdrag.parsers.microlean.axiom(tree: Tree, env: Env) → Proof

Parse an axiom.

>>> tree = lark.Lark(grammar, start="axiom", parser="lalr").parse("axiom add1_nonneg : forall x : Int, x >= x - 1")
>>> axiom(tree, Env(locals={}, globals={}))
|= ForAll(x, x >= x - 1)

Parameters:

tree (Tree)
env (Env)

Return type:

Proof

kdrag.parsers.microlean.binder(tree, env) → list[ExprRef]

Return type:: list[ExprRef]

kdrag.parsers.microlean.binders(tree, env) → list[ExprRef]

Return type:: list[ExprRef]

kdrag.parsers.microlean.define(tree: Tree, env: Env) → FuncDeclRef

Parse a definition.

>>> tree = lark.Lark(grammar, start="define", parser="lalr").parse("def add1 (x : Int) : Int := x + 1")
>>> define(tree, Env(locals={}, globals={})).defn
|= ForAll(x, add1(x) == x + 1)

Parameters:

tree (Tree)
env (Env)

Return type:

FuncDeclRef

kdrag.parsers.microlean.expr(tree, env: Env) → ExprRef

Parameters:: env (Env)
Return type:: ExprRef

kdrag.parsers.microlean.inductive(s: str, globals=None) → DatatypeSortRef

Parse an inductive datatype definition.

>>> inductive("inductive boollist where | nil : boollist | cons : Bool -> boollist -> boollist").constructor(0)
nil
>>> Nat = kd.Nat
>>> inductive("inductive foo where | mkfoo : Nat -> foo")
foo

Parameters:: s (str)
Return type:: DatatypeSortRef

kdrag.parsers.microlean.inductive_of_tree(tree: Tree, globals=None) → DatatypeSortRef

Parse an inductive datatype definition.

>>> tree = inductive_parser.parse("inductive nat where | zero : nat | succ : nat -> nat | fiz : Int -> Bool -> (Bool -> nat) -> nat")
>>> inductive_of_tree(tree).constructor(1)
succ
>>> inductive_of_tree(tree).accessor(1,0)
succ0

Parameters:: tree (Tree)
Return type:: DatatypeSortRef

kdrag.parsers.microlean.lean(s: str, globals=None) → ExprRef

Alias for parse to match Lean users’ expectations.

>>> foo = smt.Int("foo1")
>>> lean("foo + 2")
foo1 + 2

Parameters:: s (str)
Return type:: ExprRef

kdrag.parsers.microlean.parse(s: str, globals=None) → ExprRef

Parse a logical expression into an SMT expression.

>>> parse("x + 1", {"x": smt.Int("x")})
x + 1
>>> x, y = smt.Ints("x y")
>>> assert parse("forall (x y : Int), x + 1 = 0 -> x = -1").eq( smt.ForAll([x, y], x + 1 == 0, x == -1))
>>> a = smt.Real("a")
>>> assert parse("exists (a : Real), a * a = 2").eq(smt.Exists([a], a * a == 2))
>>> parse("fun (x : Int -> Int) => x 1 = 2")
Lambda(x, x[1] == 2)
>>> parse("fun (x : Int -> Int -> Int) => x 1 3 = 2")
Lambda(x, x[1][3] == 2)
>>> parse("f 3 2", {"f": smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort())})
f(3, 2)
>>> parse("fun (x : Int) (y : Real) => x + y > 0")
Lambda([x, y], ToReal(x) + y > 0)
>>> parse(r"forall (x : Int), x >= 0 /\ x < 10")
ForAll(x, And(x >= 0, x < 10))
>>> parse(r"forall (x : Int), x >= 0 && x < 10 -> x < 20")
ForAll(x, Implies(And(x >= 0, x < 10), x < 20))
>>> parse(r"exists (x : (BitVec 32) -> BitVec 8), x 8 = 5")
Exists(x, x[8] == 5)
>>> parse("fun x y (z : Int) => x + y + z", {"x": smt.Int("x"), "y": smt.Int("y")})
Lambda([x, y, z], x + y + z)
>>> parse("fun (x : 'a) => x").sort()
Array(a, a)
>>> parse("true")
True
>>> parse("[true, false]")
Concat(Unit(True), Unit(False))
>>> q = smt.Const("x", smt.TupleSort("pair", [smt.IntSort(), smt.BoolSort()])[0])
>>> parse("q.project1", {"q": q})
project1(x)
>>> parse("{x : Int | x > 0}")
Lambda(x, x > 0)
>>> parse("if true && false then 1 + 1 else 0")
If(And(True, False), 2, 0)

Parameters:: s (str)
Return type:: ExprRef

kdrag.parsers.microlean.quant(vs, body_tree, q, env) → QuantifierRef

Return type:: QuantifierRef

kdrag.parsers.microlean.sort(tree: Tree, env: Env) → SortRef

Parameters:

tree (Tree)
env (Env)

Return type:

SortRef

kdrag.parsers.microlean.start(tree: Tree, globals) → ExprRef

Parameters:: tree (Tree)
Return type:: ExprRef

kdrag.parsers.microlean.theorem(tree: Tree, env: Env) → Proof

Parse a theorem.

>>> tree = lark.Lark(grammar, start="theorem", parser="lalr").parse("theorem add1_nonneg : forall x : Int, x >= x - 1 := grind")
>>> theorem(tree, Env(locals={}, globals={}))
|= ForAll(x, x >= x - 1)

Parameters:

tree (Tree)
env (Env)

Return type:

Proof