Re: [isabelle] Difference between "char list" and that in embedded ML ?
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,
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)".
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:
(*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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and