51 at our disposal, including arrays and references, features that are less |
51 at our disposal, including arrays and references, features that are less |
52 easily emulated in HOL. In fact, we could even call some external software |
52 easily emulated in HOL. In fact, we could even call some external software |
53 from ML, e.g.\ a computer algebra system. |
53 from ML, e.g.\ a computer algebra system. |
54 |
54 |
55 It should be noted, however, that in this example you need to import the |
55 It should be noted, however, that in this example you need to import the |
56 theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to |
56 theory @{theory Code_Target_Numeral} in order to force the HOL-type @{typ nat} to |
57 be implemented by the ML-type @{text "int"}. |
57 be implemented by the ML-type @{text "int"}. |
58 |
58 |
59 \begin{graybox}\small |
59 \begin{graybox}\small |
60 \isacommand{theory}~@{text CallML}\\ |
60 \isacommand{theory}~@{text CallML}\\ |
61 \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Efficient_Nat"}\\ |
61 \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Code_Target_Numeral"}\\ |
62 ... |
62 ... |
63 \end{graybox} |
63 \end{graybox} |
64 |
64 |
65 |
65 |
66 Thus the ML implementation of |
66 Thus the ML implementation of |
67 @{const factor} must be and is of type @{text "int -> int"}. Now it is time |
67 @{const factor} must be and is of type @{text "int -> int"}. Now it is time |
68 to connect the two levels: |
68 to connect the two levels: |
69 *} |
69 *} |
70 |
70 |
71 code_const factor (SML "factor") |
71 definition factor_integer :: "integer \<Rightarrow> integer" |
|
72 where |
|
73 [code del]: "factor_integer = integer_of_nat \<circ> factor \<circ> nat_of_integer" |
|
74 |
|
75 lemma [code]: |
|
76 "factor = nat_of_integer \<circ> factor_integer \<circ> integer_of_nat" |
|
77 by (simp add: factor_integer_def fun_eq_iff) |
|
78 |
|
79 code_const factor_integer (SML "factor") |
|
80 code_reserved SML factor |
72 |
81 |
73 text{* |
82 text{* |
74 The result of this declaration is that the HOL-function @{const factor} |
83 The result of this declaration is that the HOL-function @{const factor} |
75 is executable and command |
84 is executable and command |
76 *} |
85 *} |
98 definitions can lead to compile time or run time exceptions, or to failed |
107 definitions can lead to compile time or run time exceptions, or to failed |
99 proofs. |
108 proofs. |
100 |
109 |
101 The above example was easy because we forced Isabelle (via the inclusion of the |
110 The above example was easy because we forced Isabelle (via the inclusion of the |
102 theory @{theory |
111 theory @{theory |
103 Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined |
112 Code_Target_Numeral}) to implement @{typ nat} by @{text int}, a predefined |
104 ML-type. By default, Isabelle implements, for example, the HOL-type |
113 ML-type. By default, Isabelle implements, for example, the HOL-type |
105 @{text list} by the corresponding ML-type. Thus the following variation |
114 @{text list} by the corresponding ML-type. Thus the following variation |
106 on @{const factor} also works: |
115 on @{const factor} also works: |
107 *} |
116 *} |
108 |
117 |
109 consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*) |
118 consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*) |
110 ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*) |
119 ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*) |
111 code_const factor2 (SML "factor2") |
|
112 |
120 |
113 value "factor2 4" |
121 definition factor2_integer :: "integer \<Rightarrow> integer list" |
|
122 where |
|
123 [code del]: "factor2_integer = map integer_of_nat \<circ> factor2 \<circ> nat_of_integer" |
|
124 |
|
125 lemma [code]: |
|
126 "factor2 = map nat_of_integer \<circ> factor2_integer \<circ> integer_of_nat" |
|
127 by (simp add: factor2_integer_def fun_eq_iff comp_def) |
|
128 |
|
129 code_const factor2_integer (SML "factor2") |
|
130 code_reserved SML factor2 |
114 |
131 |
115 text{* |
132 text{* |
116 The first line declares the type of @{const factor2}; the second |
133 The first line declares the type of @{const factor2}; the second |
117 gives its implementation in ML; the third makes it executable |
134 gives its implementation in ML; the third makes it executable |
118 in HOL, and the last is just a test. In this way, you can easily |
135 in HOL, and the last is just a test. In this way, you can easily |
119 interface with ML-functions whose types involve |
136 interface with ML-functions whose types involve |
120 @{text bool}, @{text int}, @{text list}, @{text option} and pairs, |
137 @{text bool}, @{text int}, @{text list}, @{text option} and pairs, |
121 only. If you have arbitrary tuples, for example, then you have to code |
138 only. If you have arbitrary tuples, for example, then you have to code |
122 them as nested pairs. |
139 them as nested pairs. |
123 |
|
124 Let us now look at how to refer to user-defined HOL-datatypes from the |
|
125 ML-level. We modify our @{const factor} example a little by introducing a new |
|
126 datatype for the result: |
|
127 *} |
140 *} |
128 |
141 |
129 datatype result = Factor nat | Prime |
142 value "factor2 4" |
130 |
|
131 consts factor' :: "nat \<Rightarrow> result" |
|
132 |
|
133 text{* |
|
134 In order to write ML-code that uses this datatype, we need to define |
|
135 this datatype at the ML-level first. The following command does just that. |
|
136 *} |
|
137 |
|
138 code_reflect Result |
|
139 datatypes result = Factor | Prime |
|
140 |
|
141 text{* |
|
142 This creates an ML-structure called @{text Result} (the name can be |
|
143 arbitrarily chosen) that contains the datatype @{typ result}. The list |
|
144 of constructors (but not their types) needs to be given. Now we can |
|
145 write ML-code that uses this datatype: |
|
146 *} |
|
147 |
|
148 ML %grayML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*} |
|
149 |
|
150 text{* |
|
151 Finally we can link the HOL and ML version of @{const factor'} as |
|
152 before: |
|
153 *} |
|
154 |
|
155 code_const factor' (SML "factor'") |
|
156 |
|
157 text{* |
|
158 Now any evaluation of the HOL function @{const factor'} will use the |
|
159 corresponding ML-function, like in the examples for @{const factor} above. |
|
160 |
|
161 In general, \isacommand{code\_reflect} can export multiple datatypes |
|
162 (separated by \isacommand{and}) and also HOL-functions: simply add a line |
|
163 \isacommand{functions} $f_1$ $f_2$ and so on. |
|
164 *} |
|
165 |
|
166 (*<*) |
|
167 value "factor' 4" |
|
168 |
143 |
169 end |
144 end |
170 (*>*) |
145 (*>*) |