src/Tools/SML/Examples.thy
author wenzelm
Sat Apr 19 17:23:05 2014 +0200 (2014-04-19)
changeset 56618 874bdedb2313
parent 56276 9e2d5e3debd3
child 58616 4257a7f2bf39
permissions -rw-r--r--
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm@56276
     1
(*  Title:      Tools/SML/Examples.thy
wenzelm@56276
     2
    Author:     Makarius
wenzelm@56276
     3
*)
wenzelm@56276
     4
wenzelm@56276
     5
header {* Standard ML within the Isabelle environment *}
wenzelm@56276
     6
wenzelm@56276
     7
theory Examples
wenzelm@56276
     8
imports Pure
wenzelm@56276
     9
begin
wenzelm@56276
    10
wenzelm@56276
    11
text {*
wenzelm@56276
    12
  Isabelle/ML is a somewhat augmented version of Standard ML, with
wenzelm@56276
    13
  various add-ons that are indispensable for Isabelle development, but
wenzelm@56276
    14
  may cause conflicts with independent projects in plain Standard ML.
wenzelm@56276
    15
wenzelm@56276
    16
  The Isabelle/Isar command 'SML_file' supports official Standard ML
wenzelm@56276
    17
  within the Isabelle environment, with full support in the Prover IDE
wenzelm@56276
    18
  (Isabelle/jEdit).
wenzelm@56276
    19
wenzelm@56276
    20
  Here is a very basic example that defines the factorial function and
wenzelm@56276
    21
  evaluates it for some arguments.
wenzelm@56276
    22
*}
wenzelm@56276
    23
wenzelm@56276
    24
SML_file "factorial.sml"
wenzelm@56276
    25
wenzelm@56276
    26
text {*
wenzelm@56276
    27
  The subsequent example illustrates the use of multiple 'SML_file'
wenzelm@56276
    28
  commands to build larger Standard ML projects.  The toplevel SML
wenzelm@56276
    29
  environment is enriched cumulatively within the theory context of
wenzelm@56276
    30
  Isabelle --- independently of the Isabelle/ML environment.
wenzelm@56276
    31
*}
wenzelm@56276
    32
wenzelm@56276
    33
SML_file "Example.sig"
wenzelm@56276
    34
SML_file "Example.sml"
wenzelm@56276
    35
wenzelm@56618
    36
wenzelm@56618
    37
text {*
wenzelm@56618
    38
  Isabelle/ML and SML share a common run-time system, but the static
wenzelm@56618
    39
  environments are separate.  It is possible to exchange toplevel bindings
wenzelm@56618
    40
  via separate commands like this.
wenzelm@56618
    41
*}
wenzelm@56618
    42
wenzelm@56618
    43
SML_export {* val f = factorial *}  -- {* re-use factorial from SML environment *}
wenzelm@56618
    44
ML {* f 42 *}
wenzelm@56618
    45
wenzelm@56618
    46
SML_import {* val println = Output.writeln *}
wenzelm@56618
    47
  -- {* re-use Isabelle/ML channel for SML *}
wenzelm@56618
    48
wenzelm@56618
    49
SML_import {* val par_map = Par_List.map *}
wenzelm@56618
    50
  -- {* re-use Isabelle/ML parallel list combinator for SML *}
wenzelm@56618
    51
wenzelm@56276
    52
end