1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Mon Mar 02 16:58:39 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,534 +0,0 @@
1.4 -theory Program
1.5 -imports Introduction
1.6 -begin
1.7 -
1.8 -section {* Turning Theories into Programs \label{sec:program} *}
1.9 -
1.10 -subsection {* The @{text "Isabelle/HOL"} default setup *}
1.11 -
1.12 -text {*
1.13 - We have already seen how by default equations stemming from
1.14 - @{command definition}/@{command primrec}/@{command fun}
1.15 - statements are used for code generation. This default behaviour
1.16 - can be changed, e.g. by providing different code equations.
1.17 - All kinds of customisation shown in this section is \emph{safe}
1.18 - in the sense that the user does not have to worry about
1.19 - correctness -- all programs generatable that way are partially
1.20 - correct.
1.21 -*}
1.22 -
1.23 -subsection {* Selecting code equations *}
1.24 -
1.25 -text {*
1.26 - Coming back to our introductory example, we
1.27 - could provide an alternative code equations for @{const dequeue}
1.28 - explicitly:
1.29 -*}
1.30 -
1.31 -lemma %quote [code]:
1.32 - "dequeue (AQueue xs []) =
1.33 - (if xs = [] then (None, AQueue [] [])
1.34 - else dequeue (AQueue [] (rev xs)))"
1.35 - "dequeue (AQueue xs (y # ys)) =
1.36 - (Some y, AQueue xs ys)"
1.37 - by (cases xs, simp_all) (cases "rev xs", simp_all)
1.38 -
1.39 -text {*
1.40 - \noindent The annotation @{text "[code]"} is an @{text Isar}
1.41 - @{text attribute} which states that the given theorems should be
1.42 - considered as code equations for a @{text fun} statement --
1.43 - the corresponding constant is determined syntactically. The resulting code:
1.44 -*}
1.45 -
1.46 -text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
1.47 -
1.48 -text {*
1.49 - \noindent You may note that the equality test @{term "xs = []"} has been
1.50 - replaced by the predicate @{term "null xs"}. This is due to the default
1.51 - setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
1.52 -
1.53 - Changing the default constructor set of datatypes is also
1.54 - possible. See \secref{sec:datatypes} for an example.
1.55 -
1.56 - As told in \secref{sec:concept}, code generation is based
1.57 - on a structured collection of code theorems.
1.58 - For explorative purpose, this collection
1.59 - may be inspected using the @{command code_thms} command:
1.60 -*}
1.61 -
1.62 -code_thms %quote dequeue
1.63 -
1.64 -text {*
1.65 - \noindent prints a table with \emph{all} code equations
1.66 - for @{const dequeue}, including
1.67 - \emph{all} code equations those equations depend
1.68 - on recursively.
1.69 -
1.70 - Similarly, the @{command code_deps} command shows a graph
1.71 - visualising dependencies between code equations.
1.72 -*}
1.73 -
1.74 -subsection {* @{text class} and @{text instantiation} *}
1.75 -
1.76 -text {*
1.77 - Concerning type classes and code generation, let us examine an example
1.78 - from abstract algebra:
1.79 -*}
1.80 -
1.81 -class %quote semigroup =
1.82 - fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
1.83 - assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.84 -
1.85 -class %quote monoid = semigroup +
1.86 - fixes neutral :: 'a ("\<one>")
1.87 - assumes neutl: "\<one> \<otimes> x = x"
1.88 - and neutr: "x \<otimes> \<one> = x"
1.89 -
1.90 -instantiation %quote nat :: monoid
1.91 -begin
1.92 -
1.93 -primrec %quote mult_nat where
1.94 - "0 \<otimes> n = (0\<Colon>nat)"
1.95 - | "Suc m \<otimes> n = n + m \<otimes> n"
1.96 -
1.97 -definition %quote neutral_nat where
1.98 - "\<one> = Suc 0"
1.99 -
1.100 -lemma %quote add_mult_distrib:
1.101 - fixes n m q :: nat
1.102 - shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
1.103 - by (induct n) simp_all
1.104 -
1.105 -instance %quote proof
1.106 - fix m n q :: nat
1.107 - show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
1.108 - by (induct m) (simp_all add: add_mult_distrib)
1.109 - show "\<one> \<otimes> n = n"
1.110 - by (simp add: neutral_nat_def)
1.111 - show "m \<otimes> \<one> = m"
1.112 - by (induct m) (simp_all add: neutral_nat_def)
1.113 -qed
1.114 -
1.115 -end %quote
1.116 -
1.117 -text {*
1.118 - \noindent We define the natural operation of the natural numbers
1.119 - on monoids:
1.120 -*}
1.121 -
1.122 -primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
1.123 - "pow 0 a = \<one>"
1.124 - | "pow (Suc n) a = a \<otimes> pow n a"
1.125 -
1.126 -text {*
1.127 - \noindent This we use to define the discrete exponentiation function:
1.128 -*}
1.129 -
1.130 -definition %quote bexp :: "nat \<Rightarrow> nat" where
1.131 - "bexp n = pow n (Suc (Suc 0))"
1.132 -
1.133 -text {*
1.134 - \noindent The corresponding code:
1.135 -*}
1.136 -
1.137 -text %quote {*@{code_stmts bexp (Haskell)}*}
1.138 -
1.139 -text {*
1.140 - \noindent This is a convenient place to show how explicit dictionary construction
1.141 - manifests in generated code (here, the same example in @{text SML}):
1.142 -*}
1.143 -
1.144 -text %quote {*@{code_stmts bexp (SML)}*}
1.145 -
1.146 -text {*
1.147 - \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
1.148 - which are the dictionary parameters.
1.149 -*}
1.150 -
1.151 -subsection {* The preprocessor \label{sec:preproc} *}
1.152 -
1.153 -text {*
1.154 - Before selected function theorems are turned into abstract
1.155 - code, a chain of definitional transformation steps is carried
1.156 - out: \emph{preprocessing}. In essence, the preprocessor
1.157 - consists of two components: a \emph{simpset} and \emph{function transformers}.
1.158 -
1.159 - The \emph{simpset} allows to employ the full generality of the Isabelle
1.160 - simplifier. Due to the interpretation of theorems
1.161 - as code equations, rewrites are applied to the right
1.162 - hand side and the arguments of the left hand side of an
1.163 - equation, but never to the constant heading the left hand side.
1.164 - An important special case are \emph{inline theorems} which may be
1.165 - declared and undeclared using the
1.166 - \emph{code inline} or \emph{code inline del} attribute respectively.
1.167 -
1.168 - Some common applications:
1.169 -*}
1.170 -
1.171 -text_raw {*
1.172 - \begin{itemize}
1.173 -*}
1.174 -
1.175 -text {*
1.176 - \item replacing non-executable constructs by executable ones:
1.177 -*}
1.178 -
1.179 -lemma %quote [code inline]:
1.180 - "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
1.181 -
1.182 -text {*
1.183 - \item eliminating superfluous constants:
1.184 -*}
1.185 -
1.186 -lemma %quote [code inline]:
1.187 - "1 = Suc 0" by simp
1.188 -
1.189 -text {*
1.190 - \item replacing executable but inconvenient constructs:
1.191 -*}
1.192 -
1.193 -lemma %quote [code inline]:
1.194 - "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
1.195 -
1.196 -text_raw {*
1.197 - \end{itemize}
1.198 -*}
1.199 -
1.200 -text {*
1.201 - \noindent \emph{Function transformers} provide a very general interface,
1.202 - transforming a list of function theorems to another
1.203 - list of function theorems, provided that neither the heading
1.204 - constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc}
1.205 - pattern elimination implemented in
1.206 - theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this
1.207 - interface.
1.208 -
1.209 - \noindent The current setup of the preprocessor may be inspected using
1.210 - the @{command print_codesetup} command.
1.211 - @{command code_thms} provides a convenient
1.212 - mechanism to inspect the impact of a preprocessor setup
1.213 - on code equations.
1.214 -
1.215 - \begin{warn}
1.216 - The attribute \emph{code unfold}
1.217 - associated with the @{text "SML code generator"} also applies to
1.218 - the @{text "generic code generator"}:
1.219 - \emph{code unfold} implies \emph{code inline}.
1.220 - \end{warn}
1.221 -*}
1.222 -
1.223 -subsection {* Datatypes \label{sec:datatypes} *}
1.224 -
1.225 -text {*
1.226 - Conceptually, any datatype is spanned by a set of
1.227 - \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
1.228 - "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
1.229 - @{text "\<tau>"}. The HOL datatype package by default registers any new
1.230 - datatype in the table of datatypes, which may be inspected using the
1.231 - @{command print_codesetup} command.
1.232 -
1.233 - In some cases, it is appropriate to alter or extend this table. As
1.234 - an example, we will develop an alternative representation of the
1.235 - queue example given in \secref{sec:intro}. The amortised
1.236 - representation is convenient for generating code but exposes its
1.237 - \qt{implementation} details, which may be cumbersome when proving
1.238 - theorems about it. Therefore, here a simple, straightforward
1.239 - representation of queues:
1.240 -*}
1.241 -
1.242 -datatype %quote 'a queue = Queue "'a list"
1.243 -
1.244 -definition %quote empty :: "'a queue" where
1.245 - "empty = Queue []"
1.246 -
1.247 -primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
1.248 - "enqueue x (Queue xs) = Queue (xs @ [x])"
1.249 -
1.250 -fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
1.251 - "dequeue (Queue []) = (None, Queue [])"
1.252 - | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
1.253 -
1.254 -text {*
1.255 - \noindent This we can use directly for proving; for executing,
1.256 - we provide an alternative characterisation:
1.257 -*}
1.258 -
1.259 -definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
1.260 - "AQueue xs ys = Queue (ys @ rev xs)"
1.261 -
1.262 -code_datatype %quote AQueue
1.263 -
1.264 -text {*
1.265 - \noindent Here we define a \qt{constructor} @{const "AQueue"} which
1.266 - is defined in terms of @{text "Queue"} and interprets its arguments
1.267 - according to what the \emph{content} of an amortised queue is supposed
1.268 - to be. Equipped with this, we are able to prove the following equations
1.269 - for our primitive queue operations which \qt{implement} the simple
1.270 - queues in an amortised fashion:
1.271 -*}
1.272 -
1.273 -lemma %quote empty_AQueue [code]:
1.274 - "empty = AQueue [] []"
1.275 - unfolding AQueue_def empty_def by simp
1.276 -
1.277 -lemma %quote enqueue_AQueue [code]:
1.278 - "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
1.279 - unfolding AQueue_def by simp
1.280 -
1.281 -lemma %quote dequeue_AQueue [code]:
1.282 - "dequeue (AQueue xs []) =
1.283 - (if xs = [] then (None, AQueue [] [])
1.284 - else dequeue (AQueue [] (rev xs)))"
1.285 - "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
1.286 - unfolding AQueue_def by simp_all
1.287 -
1.288 -text {*
1.289 - \noindent For completeness, we provide a substitute for the
1.290 - @{text case} combinator on queues:
1.291 -*}
1.292 -
1.293 -definition %quote
1.294 - aqueue_case_def: "aqueue_case = queue_case"
1.295 -
1.296 -lemma %quote aqueue_case [code, code inline]:
1.297 - "queue_case = aqueue_case"
1.298 - unfolding aqueue_case_def ..
1.299 -
1.300 -lemma %quote case_AQueue [code]:
1.301 - "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
1.302 - unfolding aqueue_case_def AQueue_def by simp
1.303 -
1.304 -text {*
1.305 - \noindent The resulting code looks as expected:
1.306 -*}
1.307 -
1.308 -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
1.309 -
1.310 -text {*
1.311 - \noindent From this example, it can be glimpsed that using own
1.312 - constructor sets is a little delicate since it changes the set of
1.313 - valid patterns for values of that type. Without going into much
1.314 - detail, here some practical hints:
1.315 -
1.316 - \begin{itemize}
1.317 -
1.318 - \item When changing the constructor set for datatypes, take care
1.319 - to provide an alternative for the @{text case} combinator
1.320 - (e.g.~by replacing it using the preprocessor).
1.321 -
1.322 - \item Values in the target language need not to be normalised --
1.323 - different values in the target language may represent the same
1.324 - value in the logic.
1.325 -
1.326 - \item Usually, a good methodology to deal with the subtleties of
1.327 - pattern matching is to see the type as an abstract type: provide
1.328 - a set of operations which operate on the concrete representation
1.329 - of the type, and derive further operations by combinations of
1.330 - these primitive ones, without relying on a particular
1.331 - representation.
1.332 -
1.333 - \end{itemize}
1.334 -*}
1.335 -
1.336 -
1.337 -subsection {* Equality and wellsortedness *}
1.338 -
1.339 -text {*
1.340 - Surely you have already noticed how equality is treated
1.341 - by the code generator:
1.342 -*}
1.343 -
1.344 -primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.345 - "collect_duplicates xs ys [] = xs"
1.346 - | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
1.347 - then if z \<in> set ys
1.348 - then collect_duplicates xs ys zs
1.349 - else collect_duplicates xs (z#ys) zs
1.350 - else collect_duplicates (z#xs) (z#ys) zs)"
1.351 -
1.352 -text {*
1.353 - \noindent The membership test during preprocessing is rewritten,
1.354 - resulting in @{const List.member}, which itself
1.355 - performs an explicit equality check.
1.356 -*}
1.357 -
1.358 -text %quote {*@{code_stmts collect_duplicates (SML)}*}
1.359 -
1.360 -text {*
1.361 - \noindent Obviously, polymorphic equality is implemented the Haskell
1.362 - way using a type class. How is this achieved? HOL introduces
1.363 - an explicit class @{class eq} with a corresponding operation
1.364 - @{const eq_class.eq} such that @{thm eq [no_vars]}.
1.365 - The preprocessing framework does the rest by propagating the
1.366 - @{class eq} constraints through all dependent code equations.
1.367 - For datatypes, instances of @{class eq} are implicitly derived
1.368 - when possible. For other types, you may instantiate @{text eq}
1.369 - manually like any other type class.
1.370 -
1.371 - Though this @{text eq} class is designed to get rarely in
1.372 - the way, a subtlety
1.373 - enters the stage when definitions of overloaded constants
1.374 - are dependent on operational equality. For example, let
1.375 - us define a lexicographic ordering on tuples
1.376 - (also see theory @{theory Product_ord}):
1.377 -*}
1.378 -
1.379 -instantiation %quote "*" :: (order, order) order
1.380 -begin
1.381 -
1.382 -definition %quote [code del]:
1.383 - "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
1.384 -
1.385 -definition %quote [code del]:
1.386 - "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
1.387 -
1.388 -instance %quote proof
1.389 -qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
1.390 -
1.391 -end %quote
1.392 -
1.393 -lemma %quote order_prod [code]:
1.394 - "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
1.395 - x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
1.396 - "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
1.397 - x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
1.398 - by (simp_all add: less_prod_def less_eq_prod_def)
1.399 -
1.400 -text {*
1.401 - \noindent Then code generation will fail. Why? The definition
1.402 - of @{term "op \<le>"} depends on equality on both arguments,
1.403 - which are polymorphic and impose an additional @{class eq}
1.404 - class constraint, which the preprocessor does not propagate
1.405 - (for technical reasons).
1.406 -
1.407 - The solution is to add @{class eq} explicitly to the first sort arguments in the
1.408 - code theorems:
1.409 -*}
1.410 -
1.411 -lemma %quote order_prod_code [code]:
1.412 - "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
1.413 - x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
1.414 - "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
1.415 - x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
1.416 - by (simp_all add: less_prod_def less_eq_prod_def)
1.417 -
1.418 -text {*
1.419 - \noindent Then code generation succeeds:
1.420 -*}
1.421 -
1.422 -text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
1.423 -
1.424 -text {*
1.425 - In some cases, the automatically derived code equations
1.426 - for equality on a particular type may not be appropriate.
1.427 - As example, watch the following datatype representing
1.428 - monomorphic parametric types (where type constructors
1.429 - are referred to by natural numbers):
1.430 -*}
1.431 -
1.432 -datatype %quote monotype = Mono nat "monotype list"
1.433 -(*<*)
1.434 -lemma monotype_eq:
1.435 - "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv>
1.436 - eq_class.eq tyco1 tyco2 \<and> eq_class.eq typargs1 typargs2" by (simp add: eq)
1.437 -(*>*)
1.438 -
1.439 -text {*
1.440 - \noindent Then code generation for SML would fail with a message
1.441 - that the generated code contains illegal mutual dependencies:
1.442 - the theorem @{thm monotype_eq [no_vars]} already requires the
1.443 - instance @{text "monotype \<Colon> eq"}, which itself requires
1.444 - @{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
1.445 - recursive @{text instance} and @{text function} definitions,
1.446 - but the SML serialiser does not support this.
1.447 -
1.448 - In such cases, you have to provide your own equality equations
1.449 - involving auxiliary constants. In our case,
1.450 - @{const [show_types] list_all2} can do the job:
1.451 -*}
1.452 -
1.453 -lemma %quote monotype_eq_list_all2 [code]:
1.454 - "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
1.455 - eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
1.456 - by (simp add: eq list_all2_eq [symmetric])
1.457 -
1.458 -text {*
1.459 - \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
1.460 -*}
1.461 -
1.462 -text %quote {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
1.463 -
1.464 -
1.465 -subsection {* Explicit partiality *}
1.466 -
1.467 -text {*
1.468 - Partiality usually enters the game by partial patterns, as
1.469 - in the following example, again for amortised queues:
1.470 -*}
1.471 -
1.472 -definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
1.473 - "strict_dequeue q = (case dequeue q
1.474 - of (Some x, q') \<Rightarrow> (x, q'))"
1.475 -
1.476 -lemma %quote strict_dequeue_AQueue [code]:
1.477 - "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
1.478 - "strict_dequeue (AQueue xs []) =
1.479 - (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
1.480 - by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
1.481 -
1.482 -text {*
1.483 - \noindent In the corresponding code, there is no equation
1.484 - for the pattern @{term "AQueue [] []"}:
1.485 -*}
1.486 -
1.487 -text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
1.488 -
1.489 -text {*
1.490 - \noindent In some cases it is desirable to have this
1.491 - pseudo-\qt{partiality} more explicitly, e.g.~as follows:
1.492 -*}
1.493 -
1.494 -axiomatization %quote empty_queue :: 'a
1.495 -
1.496 -definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
1.497 - "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
1.498 -
1.499 -lemma %quote strict_dequeue'_AQueue [code]:
1.500 - "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
1.501 - else strict_dequeue' (AQueue [] (rev xs)))"
1.502 - "strict_dequeue' (AQueue xs (y # ys)) =
1.503 - (y, AQueue xs ys)"
1.504 - by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
1.505 -
1.506 -text {*
1.507 - Observe that on the right hand side of the definition of @{const
1.508 - "strict_dequeue'"} the constant @{const empty_queue} occurs
1.509 - which is unspecified.
1.510 -
1.511 - Normally, if constants without any code equations occur in a
1.512 - program, the code generator complains (since in most cases this is
1.513 - not what the user expects). But such constants can also be thought
1.514 - of as function definitions with no equations which always fail,
1.515 - since there is never a successful pattern match on the left hand
1.516 - side. In order to categorise a constant into that category
1.517 - explicitly, use @{command "code_abort"}:
1.518 -*}
1.519 -
1.520 -code_abort %quote empty_queue
1.521 -
1.522 -text {*
1.523 - \noindent Then the code generator will just insert an error or
1.524 - exception at the appropriate position:
1.525 -*}
1.526 -
1.527 -text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
1.528 -
1.529 -text {*
1.530 - \noindent This feature however is rarely needed in practice.
1.531 - Note also that the @{text HOL} default setup already declares
1.532 - @{const undefined} as @{command "code_abort"}, which is most
1.533 - likely to be used in such situations.
1.534 -*}
1.535 -
1.536 -end
1.537 -
1.538 \ No newline at end of file