Open tothtamas28 opened 3 months ago
A small script to print the AST for a .lean
file:
import Lean
open Lean
open Lean.Parser
def main (args : List String): IO Unit := do
let env ← mkEmptyEnvironment
let fname := args.get! 0
let tsyntax ← testParseFile env fname
IO.println tsyntax
$ lean --run ParseModule.lean ParseModule.lean
The transformation should be based on
definition.kore
. However, for ease of exposition, examples will be based on the.k
definition.Prelude
We need a manual Lean 4 implementation of (parts of)
domains.md
. The implementation should define sorts likeInt
andMap
, functions over them, and provide useful theorems. Stubs for hooked functions, as well as non-hooked function implementations (hopefully) can be auto-generated.We need to decide if we want to map sorts directly (e.g. K
Int
to Lean 4Int
), or add an extra layer (KInt.mk : Int -> KInt
). In the direct mapping case,abbrev
is useful for aliasing Lean 4 types:The mapping is obvious for some sorts, for others, we might need a custom implementation:
Bool
Bool
Int
Int
String
String
Bytes
ByteArray
List
List KItem
Set
Map
The sort
K
with constructorsdotk : K
andkseq : KItem -> K
can either be modeled asList KItem
, or as generated fromdefinition.kore
.User defined sorts
Sorts that depend on each other should be put in a
mutual
block:It's probably fine to model user lists as
List
.Injection
The sort of ad-hoc polymorphism provided by injections can be modeled using type classes.
It is probably possible to define a transitivity instance to reduce the number of explicitly defined instances, but that complicates type class resolution.
Unfortunately, implementing the
inj
function is not straightforward. To demonstrate the problem, considerHere, we need
Without a deeper embedding, this does not seem directly feasible, but approximations are possible.
Axiomatic approach
Here, we just assert the function and its transitivity. On the downside, all functions calling
inj
have to be markednoncomputable
, so we lose computability.Constructive approach
Here, as expected,
On the downside, the constructors induce spurious terms like
KItem.inj_aexp (AExp.inj_int (KInt.mk 0))
. Since we never refer to such terms in the transition relation, this is probably acceptable.Rewrite rules
It seems straightforward to get an overapproximation of the transition relation by neglecting rule priorities and ensures clauses (and probably other finer details we're just not aware yet).
Free variables become implicit arguments,
requires
becomes an antecedent, and the LHS and RHS are mapped directly.Functions
Ideally, we can map K functions to Lean 4 functions. So far, this seems to be the most challenging part of the transformation. The reason for this is a discrepancy in representation. K function rules have a priority, a
requires
and a pattern to match. These induceif
andmatch
expressions, and the cases for the latter need to be non-overlapping and total.We need a best effort transformation that handles at least the simple cases (like
foo
below). We might also be able to rewrite some functions to a form that's better suited for the transformation. For the rest of the cases, we can still generate a signature, and either handle them axiomatically (by generating theorems fromsimplification
rules), or implement them manually.Totality
The generated Lean 4 functions have to be total. We can handle this by returning
Option
from non-total functions, then expect a proof of definedness for rewrite rules:Here, we implicitly assume the
requires
clauses are non-overlapping (hopefully K enforces this to some extent).Note that we could mark
foo
total
in K. In these case, we can auto generate a proof obligation:From this, we can get the witness for taking rewrite step
do-foo
. An even better solution to generate inline proofs / proof stubs for fallthrough cases:Then the
Option
wrapper and the extra implication can even be omitted:Code generation
The code generator should be implemented in a way that auto generated vs user supplied code is separated.
Also, code generation should be based on an internal model of the generated Lean 4 program (as opposed to appending strings directly as in
ModuleToKore
). In one extreme, the model is the Lean 4 abstract syntax, but full generality is not necessary for our purposes. We should check if there's a Python package that implements the Lean 4 AST.Files representing Lean 4 abstract syntax: