Search code examples
isabelle

Isabelle: No code equations for the function

Here is my theory that gets OK-state up to the code generation:

theory Max_Of_Two_Integers
  imports (* Main *)
    "../Imperative_HOL" 
    Subarray
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"  
begin

function two_integer_max :: "nat ⇒ nat ⇒ nat Heap"
  where
 "two_integer_max first second =
     (if (first > second)  then
        return first
      else
        return second) "
  by pat_completeness auto

code_reserved SML upto

definition "example = do {
   a ← two_integer_max 1 2;
   return a
  }"

export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_impL

(*    
value "example"
 *)

end

Code generation creates output about error:

No code equations for two_integer_max

I am closely following https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html and I am using the same imports and the same syntax, but still - this error. I guess - the code generator has problems with unspecified generation for the two_integer_max, but Imperative_Quicksort managers to generate the more complex code involving similar structures.

Of course, I am reading Chapter 2 from https://isabelle.in.tum.de/doc/codegen.pdf about code equations but it would be nice to move quickly on and build the remaining pipeline and study theory intricacies when the basic pipeline is working.

Maybe there is tracing facility that allows to check the intermediate step of the code generation?

When I am adding

termination by auto

then that line fails with

Failed to finish proof⌂:
goal (1 subgoal):
1. ⋀a b. two_integer_max_dom (a, b)

Maybe this lack for termination proof prohibits the code generation? I am still studying how to complete this termination proof..

Solution

  • You can add the termination proof with:

    termination by size_change

    The method size_change is a simple heuristic for termination proofs. For more complex cases you can often use the relation method instead.

    Or you can use fun instead of function. In that case you neither need the well-definedness proof (by pat_completeness auto) nor the manual termination proof.