7 theory Examples |
7 theory Examples |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 Isabelle/ML is a somewhat augmented version of Standard ML, with |
12 Isabelle/ML is a somewhat augmented version of Standard ML, with various |
13 various add-ons that are indispensable for Isabelle development, but |
13 add-ons that are indispensable for Isabelle development, but may cause |
14 may cause conflicts with independent projects in plain Standard ML. |
14 conflicts with independent projects in plain Standard ML. |
15 |
15 |
16 The Isabelle/Isar command 'SML_file' supports official Standard ML |
16 The Isabelle/Isar command \<^theory_text>\<open>SML_file\<close> supports official Standard ML within |
17 within the Isabelle environment, with full support in the Prover IDE |
17 the Isabelle environment, with full support in the Prover IDE |
18 (Isabelle/jEdit). |
18 (Isabelle/jEdit). |
19 |
19 |
20 Here is a very basic example that defines the factorial function and |
20 Here is a very basic example that defines the factorial function and |
21 evaluates it for some arguments. |
21 evaluates it for some arguments. |
22 \<close> |
22 \<close> |
23 |
23 |
24 SML_file "factorial.sml" |
24 SML_file "factorial.sml" |
25 |
25 |
26 text \<open> |
26 text \<open> |
27 The subsequent example illustrates the use of multiple 'SML_file' |
27 The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands |
28 commands to build larger Standard ML projects. The toplevel SML |
28 to build larger Standard ML projects. The toplevel SML environment is |
29 environment is enriched cumulatively within the theory context of |
29 enriched cumulatively within the theory context of Isabelle --- |
30 Isabelle --- independently of the Isabelle/ML environment. |
30 independently of the Isabelle/ML environment. |
31 \<close> |
31 \<close> |
32 |
32 |
33 SML_file "Example.sig" |
33 SML_file "Example.sig" |
34 SML_file "Example.sml" |
34 SML_file "Example.sml" |
35 |
35 |
36 |
36 |
37 text \<open> |
37 text \<open> |
38 Isabelle/ML and SML share a common run-time system, but the static |
38 Isabelle/ML and SML share a common run-time system, but the static |
39 environments are separate. It is possible to exchange toplevel bindings |
39 environments are separate. It is possible to exchange toplevel bindings via |
40 via separate commands like this. |
40 separate commands like this. |
41 \<close> |
41 \<close> |
42 |
42 |
43 SML_export \<open>val f = factorial\<close> -- \<open>re-use factorial from SML environment\<close> |
43 SML_export \<open>val f = factorial\<close> \<comment> \<open>re-use factorial from SML environment\<close> |
44 ML \<open>f 42\<close> |
44 ML \<open>f 42\<close> |
45 |
45 |
46 SML_import \<open>val println = Output.writeln\<close> |
46 SML_import \<open>val println = Output.writeln\<close> |
47 -- \<open>re-use Isabelle/ML channel for SML\<close> |
47 \<comment> \<open>re-use Isabelle/ML channel for SML\<close> |
48 |
48 |
49 SML_import \<open>val par_map = Par_List.map\<close> |
49 SML_import \<open>val par_map = Par_List.map\<close> |
50 -- \<open>re-use Isabelle/ML parallel list combinator for SML\<close> |
50 \<comment> \<open>re-use Isabelle/ML parallel list combinator for SML\<close> |
51 |
51 |
52 end |
52 end |