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



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




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