(*<*)+
−
theory CallML+
−
imports "~~/src/HOL/Number_Theory/Primes" 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+
−
  verify some complicated algorithm, have the algorithm produce an easily+
−
  checkable certificate. For example, rather than verify a primality test,+
−
  have the test produce a factor of the input as a witness to+
−
  non-primality. This is only an example, and we ignore the converse+
−
  certificate, that for primality, although it, too, can be treated in the+
−
  same manner. +
−
+
−
  The example we are looking at here is an ML function for finding a factor +
−
  of a number. We first declare its type:+
−
*}+
−
+
−
consts factor :: "nat \<Rightarrow> nat"+
−
+
−
text{* +
−
  Its definition will be given in ML below. 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{*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"}. 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{*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{*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+
−
(*>*)+
−