Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Examples.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      Tools/SML/Examples.thy
    Author:     Makarius
*)

section \<open>Standard ML within the Isabelle environment\<close>

theory Examples
  imports Pure
begin

text \<open>
  Isabelle/ML is a somewhat augmented version of Standard ML, with various
  add-ons that are indispensable for Isabelle development, but may cause
  conflicts with independent projects in plain Standard ML.

  The Isabelle/Isar command \<^theory_text>\<open>SML_file\<close> supports official Standard ML within
  the Isabelle environment, with full support in the Prover IDE
  (Isabelle/jEdit).

  Here is a very basic example that defines the factorial function and
  evaluates it for some arguments.
\<close>

SML_file \<open>factorial.sml\<close>

text \<open>
  The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
  to build larger Standard ML projects. The toplevel SML environment is
  enriched cumulatively within the theory context of Isabelle ---
  independently of the Isabelle/ML environment.
\<close>

SML_file \<open>Example.sig\<close>
SML_file \<open>Example.sml\<close>

text \<open>
  Isabelle/ML and SML share a common run-time system, but the static
  environments are separate. It is possible to exchange toplevel bindings via
  separate commands like this.
\<close>

SML_export \<open>val f = factorial\<close>  \<comment> \<open>re-use factorial from SML environment\<close>
ML \<open>f 42\<close>

SML_import \<open>val println = Output.writeln\<close>
  \<comment> \<open>re-use Isabelle/ML channel for SML\<close>

SML_import \<open>val par_map = Par_List.map\<close>
  \<comment> \<open>re-use Isabelle/ML parallel list combinator for SML\<close>

end

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.