Generate function definitions

[tothtamas28]

Depends on: #4726

Suppose we have a function production

syntax Foo ::= foo ( <params> )

The general structure of a function rule is the following:

rule foo ( <args_i> ) => <rhs_i> requires <req_i> [priority(<prio_i>)]

First, we order rules by priority. This allows the following defintion:

def foo <params> := foo_pgroup_1 <params> <|> foo_pgroup_2 <params> <|> ...

where foo_pgroup_i is a function representing all rules in priority group i. These helpers are combined using <|> in increasing order of priority, i.e., if a group with lower priority fails to yield a result, then the next group is tried, etc.

In order for the function to be well-defined, within each priority group, for a given concrete input, there must be at most one matching rule. There are three cases.

No requires clauses

def foo_pgroup_i <params> :=
  | <args_1> => some <rhs_1>
  | <args_2> => some <rhs_2>
  ...
  | _ => none

Strictly speaking, this mapping is faithful only if the patterns are non-overlapping, as the order in which patterns are defined matters in Lean. In the presence of overlapping patterns, the K function is only well defined if there's confluence of values, thus it might happen that a non-well-defined K function is translated to a well-defined Lean function.

Only a single pattern on the LHS (modulo alpha renaming)

In this case, it has to be ensured that requires clauses are non-overlapping. We can generate a theorem stub (or multiple ones, for each pair of clauses) to encode the proof obligation. Then the function definition can be implemented using if-then-else:

def foo_pgroup_i <params> :=
  | <args> =>
    if <req_1> then some <rhs_1>
    else if <req_2> then some <rhs2>
    else if ...
    else none
  | _ => none

The general case

I.e., there are requires clasues, and there are various patterns on the left hand sides of rules. Such a function can be well defined (even if the LHS patterns are overlapping), consider

rule foo ( X, 0 ) => 0 requires X =/=Int 0
rule foo ( 0, Y ) => 1 requires Y =/=Int 0

Group rules by LHS pattern. Then generate a helper function as per the previous case for each group. Combine the cases with <|> as for priority groups.

Similarly to the previous case though, a theorem stub (or multiple ones, for each pair of helpers) has to be generated that states well-definedness (i.e. at most one of the helpers returns some).

[ehildenb]

Let's leave all function uninterpreted until we run into that issue, so we only handle the simplest cases first, and then leave uninterpreted functions after that.

[tothtamas28]

Let's leave all function uninterpreted until we run into that issue, so we only handle the simplest cases first, and then leave uninterpreted functions after that.

So the generation process should be the following:

• Generate a def.
• If not possible, generate
  • An axiom for the function declaration.
  • An axiom for each function rule.

In both cases:

• Generate a theorem stub for each simplification rule.

Implementation will start with all functions uninterpreted, then will be incrementally refined to be able to generate definitions for more and more complex case.