[isabelle] Difference between "char list" and that in embedded ML ?

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.