Email Gateway (Aug 22 2022 at 15:41): Email Gateway (Aug 22 2022 at 15:41):From: ducis <ducis_cn@126.com>
Dear friends,
I'm a new user to Isabelle/HOL, trying to loading some external data following
the instruction in "A.4 Calling ML Functions from within HOL." in "The Isabelle Cookbook (draft)".
While I was able to get the example to work, I am unable to modify it to produce string output.
Neither have I found such cases on Stackoverflow or in the PDFs accompanying the distribution.
For example, I have the following code:
===================================================================
ML ‹
(*fun ls x = Isabelle_System.bash_output ("ls " ^ (String.implode x)) |> fst |> String.explode;*)
fun lsA n = if n=4 then [] else ([]:char list);
fun lsB n = if n=4 then "" else "abc";
fun lsC n = if n=4 then 5 else 10;
›
consts lsAA :: "nat ⇒ char list"
definition ls1 :: "integer ⇒ char list"
where [code del]: "ls1 = lsAA ∘ nat_of_integer"
lemma [code]: "lsAA = ls1 ∘ integer_of_nat" by (simp add: ls1_def fun_eq_iff)
code_printing constant ls1 ⇀ (SML) "lsA"
consts lsBB :: "nat ⇒ string"
definition ls2 :: "integer ⇒ string"
where [code del]: "ls2 = lsBB ∘ nat_of_integer"
lemma [code]: "lsBB = ls2 ∘ integer_of_nat" by (simp add: ls2_def fun_eq_iff)
code_printing constant ls2 ⇀ (SML) "lsB"
consts lsCC :: "nat ⇒ nat"
definition ls3 :: "integer ⇒ integer"
where [code del]: "ls3 = integer_of_nat ∘ lsCC ∘ nat_of_integer"
lemma [code]: "lsCC = nat_of_integer ∘ ls3 ∘ integer_of_nat" by (simp add: ls3_def fun_eq_iff)
code_printing constant ls3 ⇀ (SML) "lsC"
value "lsAA 1" (* outputs "ls1 1" :: "char list" *)
value "lsBB 1" (* outputs "ls2 1" :: "char list" *)
value "lsCC 1" (* outputs "10" :: "nat" *)
=====================================================================
It seems that the result of calling ML functions lsA and lsB fail to be converted into the "char list" in the Isabelle context.
How could I have ' value "lsAA 1" ' or ' value "lsBB 1" ' to produce ' [] :: "char list" ' or ' "abc" :: "char list" ?
And how can the ML function take a "char list" as its input?
Best,
Du
Email Gateway (Aug 22 2022 at 15:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Du,
The character types in Isabelle/HOL and in SML (or Isabelle/ML) are by default not
connected to each other. The only HOL types for exchanging data between Isabelle/HOL
functions and ML code are unit, bool, list, integer, and String.literal. The Isabelle/HOL
library defines a few further types, e.g., char in ~~/src/HOL/Library/Code_Char". If you
import this theory, then the generated code will use the default SML char type for HOL
characters, and your code_printing adaptations work.
However, note that you should make sure that your SML implementation correspond to their
HOL specification. As is, lsAA, lsBB and lsCC are unspecified. This is fine as long as
your implementations lsA, lsB, and lsC do not depend on side effects.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 15:43):From: Makarius <makarius@sketis.net>
On 04/07/17 18:49, ducis wrote:
I'm a new user to Isabelle/HOL, trying to loading some external data following
the instruction in "A.4 Calling ML Functions from within HOL." in "The Isabelle Cookbook (draft)".
I did not follow the further development of this Cookbook project in
recent years, and can't say how relevant it is today for using Isabelle/ML.
The main manual for Isabelle/ML programming within the official
distribution is called "implementation" (e.g. see the Documentation
panel in the Prover IDE).
For example, I have the following code:
===================================================================
ML ‹
(*fun ls x = Isabelle_System.bash_output ("ls " ^ (String.implode x)) |> fst |> String.explode;*)
fun lsA n = if n=4 then [] else ([]:char list);
fun lsB n = if n=4 then "" else "abc";
fun lsC n = if n=4 then 5 else 10;
›
consts lsAA :: "nat ⇒ char list"
definition ls1 :: "integer ⇒ char list"
where [code del]: "ls1 = lsAA ∘ nat_of_integer"
lemma [code]: "lsAA = ls1 ∘ integer_of_nat" by (simp add: ls1_def fun_eq_iff)
code_printing constant ls1 ⇀ (SML) "lsA"
What is the motivation for using HOL -> ML code generation in the first
place? You can write Isabelle/ML sources directly, e.g. to produce
logical term syntax and feed it into the formal context, lets say in a
goal state or as definitions in the target theory.
Here is a minimal example.
The result of "ls" as a term of the HOL logic:
ML ‹
fun ls_term dir =
Isabelle_System.bash_output ("ls " ^ File.bash_path dir)
|> #1 |> HOLogic.mk_string;
›
Note that giving arguments to external processes (done via GNU bash
here) always requires proper quoting. The File.bash_path function of
Isabelle/ML does that in a robust way.
A concrete example, printed in regular notation:
ML ‹
val t = ls_term (Path.explode "$ISABELLE_HOME/src");
val ctxt = @{context};
writeln (Syntax.string_of_term ctxt t);
›
This demonstrates how to define a constant in the target theory:
ML ‹
fun ls_definition binding dir =
Local_Theory.define ((binding, NoSyn), ((Thm.def_binding binding, []),
ls_term dir));
›
local_setup ‹#2 o ls_definition @{binding test} (Path.explode
"$ISABELLE_HOME/src")›
term test
thm test_def
I recommend to use the Prover IDE to explore these ML snippets, e.g. to
see inferred types of sub-expressions and to follow formal links to the
definitions.
If you want to browse formally through the main Isabelle/ML corpus, you
need to open "$ISABELLE_HOME/src/Pure/ROOT.ML" to get to active source
files eventually, such as
"$ISABELLE_HOME/src/Pure/System/isabelle_system.ML"
It is also important to look at examples -- always in the formal Prover IDE.
Makarius
Last updated: Apr 26 2024 at 04:17 UTC