equal
deleted
inserted
replaced
32 |
32 |
33 |
33 |
34 subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *} |
34 subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *} |
35 |
35 |
36 text {* |
36 text {* |
37 In a HOL theory, the @{command datatype} and @{command |
37 In a HOL theory, the @{command_def datatype} and @{command_def |
38 definition}/@{command primrec}/@{command fun} declarations form the |
38 definition}/@{command_def primrec}/@{command_def fun} declarations |
39 core of a functional programming language. By default equational |
39 form the core of a functional programming language. By default |
40 theorems stemming from those are used for generated code, therefore |
40 equational theorems stemming from those are used for generated code, |
41 \qt{naive} code generation can proceed without further ado. |
41 therefore \qt{naive} code generation can proceed without further |
|
42 ado. |
42 |
43 |
43 For example, here a simple \qt{implementation} of amortised queues: |
44 For example, here a simple \qt{implementation} of amortised queues: |
44 *} |
45 *} |
45 |
46 |
46 datatype %quote 'a queue = AQueue "'a list" "'a list" |
47 datatype %quote 'a queue = AQueue "'a list" "'a list" |
69 text {* \noindent resulting in the following code: *} |
70 text {* \noindent resulting in the following code: *} |
70 |
71 |
71 text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} |
72 text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} |
72 |
73 |
73 text {* |
74 text {* |
74 \noindent The @{command export_code} command takes a space-separated |
75 \noindent The @{command_def export_code} command takes a |
75 list of constants for which code shall be generated; anything else |
76 space-separated list of constants for which code shall be generated; |
76 needed for those is added implicitly. Then follows a target |
77 anything else needed for those is added implicitly. Then follows a |
77 language identifier and a freely chosen module name. A file name |
78 target language identifier and a freely chosen module name. A file |
78 denotes the destination to store the generated code. Note that the |
79 name denotes the destination to store the generated code. Note that |
79 semantics of the destination depends on the target language: for |
80 the semantics of the destination depends on the target language: for |
80 @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text |
81 @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text |
81 Haskell} it denotes a \emph{directory} where a file named as the |
82 Haskell} it denotes a \emph{directory} where a file named as the |
82 module name (with extension @{text ".hs"}) is written: |
83 module name (with extension @{text ".hs"}) is written: |
83 *} |
84 *} |
84 |
85 |