(*<*)
theory CallML
imports "~~/src/HOL/Number_Theory/Primes" 
        "~~/src/HOL/Library/Efficient_Nat"
begin
(*>*)

section {* Calling ML Functions from within HOL \label{rec:callml} *}

text{* 
  {\bf Problem:} 
  How to call ML functions from within HOL?\smallskip

  {\bf Solution:} This can be achieved with \isacommand{code\_const}
  and \isacommand{code\_reflect}.\smallskip


  To make it clear we mean here calling unverified ML functions from within
  HOL! The motivation is the paradigm of \emph{result checking}: rather than
  verifying some complicated algorithm, have the algorithm produce an easily
  checkable certificate. For example, instead of verifying an algorithm for 
  testing non-primality, have an algorithm that produces a factor as a witness to
  non-primality. 

  The algorithm is an ML function finding a factor of a number. We first 
  declare its type:
*}

consts factor :: "nat \<Rightarrow> nat"

text{* 
  Its definition will be given below in ML. But the whole point is that
  we can prove non-primality via @{const factor}, no matter what its
  actual definition is: 
*}

lemma factor_non_prime:
  "let k = factor n in k \<noteq> 1 \<and> k \<noteq> n \<and> k dvd n \<Longrightarrow> \<not> prime n"
  by (auto simp: prime_nat_def Let_def)

text{* 
  Note that the premise is executable once we have defined 
  @{const factor}. Here is a trivial definition in ML: 
*}

ML %grayML{*fun factor n = if n = 4 then 2 else 1*}

text{* 
  Of course this trivial definition of @{const factor} could have been given
  directly in HOL rather than ML. But by going to the ML level, all of ML is
  at our disposal, including arrays and references, features that are less
  easily emulated in HOL. In fact, we could even call some external software
  from ML, e.g.\ a computer algebra system.

  It should be noted, however, that in this example you need to import the
  theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to
  be implemented by the ML-type @{text "int"}. 

  \begin{graybox}\small
  \isacommand{theory}~@{text CallML}\\
  \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Efficient_Nat"}\\
  ...
  \end{graybox}


  Thus the ML implementation of
  @{const factor} must be and is of type @{text "int -> int"}. Now it is time
  to connect the two levels:
*}

code_const factor (SML "factor")

text{* 
  The result of this declaration is that the HOL-function @{const factor} 
  is executable and command 
*}

value "factor 4"

text{* 
  yields the expected result @{text 2}. Similarly we can prove that
  @{text 4} is not prime: 
*}

lemma "\<not> prime (4::nat)"
  apply(rule factor_non_prime)
  apply eval
  done

text{* 
  Note, however, the command \isacommand{code\_const} cannot check that the ML function
  has the required type. Therefore in the worst case a type mismatch will be detected by
  the ML-compiler when we try to evaluate an expression involving @{const
  factor}. It could also happen that @{const factor} is (accidentally)
  redefined on the ML level later on. But remember that we do not assume
  anything about @{const factor} on the HOL-level. Hence no definition of
  @{const factor} can ever lead to an incorrect proof. Of course ``wrong''
  definitions can lead to compile time or run time exceptions, or to failed
  proofs.

  The above example was easy because we forced Isabelle (via the inclusion of the
  theory @{theory
  Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined 
  ML-type.  By default, Isabelle implements, for example, the HOL-type 
  @{text list} by the corresponding ML-type. Thus the following variation 
  on @{const factor} also works: 
*}

consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*)
ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)
code_const factor2 (SML "factor2")

value "factor2 4"

text{* 
  The first line declares the type of @{const factor2}; the second
  gives its implementation in ML; the third makes it executable 
  in HOL, and the last is just a test.  In this way, you can easily 
  interface with ML-functions whose types involve 
  @{text bool}, @{text int}, @{text list}, @{text option} and pairs, 
  only. If you have arbitrary tuples, for example, then you have to code 
  them as nested pairs.

  Let us now look at how to refer to user-defined HOL-datatypes from the
  ML-level. We modify our @{const factor} example a little by introducing a new
  datatype for the result: 
*}

datatype result = Factor nat | Prime

consts factor' :: "nat \<Rightarrow> result"

text{* 
  In order to write ML-code that uses this datatype, we need to define
  this datatype at the ML-level first. The following command does just that. 
*}

code_reflect Result
  datatypes result = Factor | Prime

text{* 
  This creates an ML-structure called @{text Result} (the name can be
  arbitrarily chosen) that contains the datatype @{typ result}. The list 
  of constructors (but not their types) needs to be given. Now we can 
  write ML-code that uses this datatype: 
*}

ML %grayML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*}

text{* 
  Finally we can link the HOL and ML version of @{const factor'} as
  before: 
*}

code_const factor' (SML "factor'")

text{* 
  Now any evaluation of the HOL function @{const factor'} will use the
  corresponding ML-function, like in the examples for @{const factor} above.

  In general, \isacommand{code\_reflect} can export multiple datatypes 
  (separated by \isacommand{and}) and also HOL-functions: simply add a line
  \isacommand{functions} $f_1$ $f_2$ and so on.
*}

(*<*)
value "factor' 4"

end
(*>*)