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



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

On 04/07/17 18:49, ducis wrote:


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





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