*To*: ducis <ducis_cn at 126.com>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Difference between "char list" and that in embedded ML ?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 5 Jul 2017 12:26:43 +0200*In-reply-to*: <9d18c12.b3e8.15d0e8177b1.Coremail.ducis_cn@126.com>*References*: <mailman.43023.1498829550.832.cl-isabelle-users@lists.cam.ac.uk> <9d18c12.b3e8.15d0e8177b1.Coremail.ducis_cn@126.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.1

Dear Du,

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

**References**:

- Previous by Date: [isabelle] Difference between "char list" and that in embedded ML ?
- Next by Date: Re: [isabelle] Difference between "char list" and that in embedded ML ?
- Previous by Thread: [isabelle] Difference between "char list" and that in embedded ML ?
- Next by Thread: Re: [isabelle] Difference between "char list" and that in embedded ML ?
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list