diff --git a/thys/Clean/src/Clean.thy b/thys/Clean/src/Clean.thy --- a/thys/Clean/src/Clean.thy +++ b/thys/Clean/src/Clean.thy @@ -1,1425 +1,1425 @@ (****************************************************************************** * Clean * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) (* * Clean --- a basic abstract ("shallow") programming language for test and proof. * Burkhart Wolff and Frédéric Tuong, LRI, Univ. Paris-Saclay, France *) chapter \The Clean Language\ theory Clean imports Optics Symbex_MonadSE keywords "global_vars" "local_vars_test" :: thy_decl and "returns" "pre" "post" "local_vars" "variant" and "function_spec" :: thy_decl and "rec_function_spec" :: thy_decl begin text\Clean (pronounced as: ``C lean'' or ``Céline'' [selin]) is a minimalistic imperative language with C-like control-flow operators based on a shallow embedding into the ``State Exception Monads'' theory formalized in \<^file>\MonadSE.thy\. It strives for a type-safe notation of program-variables, an incremental construction of the typed state-space in order to facilitate incremental verification and open-world extensibility to new type definitions intertwined with the program definition. It comprises: \begin{itemize} \item C-like control flow with \<^term>\break\ and \<^term>\return\, \item global variables, \item function calls (seen as monadic executions) with side-effects, recursion and local variables, \item parameters are modeled via functional abstractions (functions are monads); a passing of parameters to local variables might be added later, \item direct recursive function calls, \item cartouche syntax for \\\-lifted update operations supporting global and local variables. \end{itemize} Note that Clean in its current version is restricted to \<^emph>\monomorphic\ global and local variables as well as function parameters. This limitation will be overcome at a later stage. The construction in itself, however, is deeply based on parametric polymorphism (enabling structured proofs over extensible records as used in languages of the ML family \<^url>\http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/21num.pdf\ and Haskell \<^url>\https://www.schoolofhaskell.com/user/fumieval/extensible-records\). \ (*<*) text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ (*>*) section\A High-level Description of the Clean Memory Model\ subsection\A Simple Typed Memory Model of Clean: An Introduction \ text\ Clean is based on a ``no-frills'' state-exception monad \<^theory_text>\type_synonym ('o, '\) MON\<^sub>S\<^sub>E = \'\ \ ('o \ '\)\\ with the usual definitions of \<^term>\bind\ and \<^term>\unit\. In this language, sequence operators, conditionals and loops can be integrated. \ text\From a concrete program, the underlying state \<^theory_text>\'\\ is \<^emph>\incrementally\ constructed by a sequence of extensible record definitions: \<^enum> Initially, an internal control state is defined to give semantics to \<^term>\break\ and \<^term>\return\ statements: \begin{isar} record control_state = break_val :: bool return_val :: bool \end{isar} \<^theory_text>\control_state\ represents the $\sigma_0$ state. \<^enum> Any global variable definition block with definitions $a_1 : \tau_1$ $\dots$ $a_n : \tau_n$ is translated into a record extension: \begin{isar} record \$_{n+1}$ = \$_n$ + a$_1$ :: $\tau_1$; ...; $a_n$ :: $\tau_n$ \end{isar} \<^enum> Any local variable definition block (as part of a procedure declaration) with definitions $a_1 : \tau_1$ $\dots$ $a_n : \tau_n$ is translated into the record extension: \begin{isar} record \$_{n+1}$ = \$_n$ + a$_1$ :: $\tau_1$ list; ...; $a_n$ :: $\tau_n$ list; result :: $\tau_{result-type}$ list; \end{isar} where the \<^typ>\_ list\-lifting is used to model a \<^emph>\stack\ of local variable instances in case of direct recursions and the \<^term>\result_value\ used for the value of the \<^term>\return\ statement.\ text \ The \<^theory_text>\record\ package creates an \<^theory_text>\'\\ extensible record type \<^theory_text>\'\ control_state_ext\ where the \<^theory_text>\'\\ stands for extensions that are subsequently ``stuffed'' in them. Furthermore, it generates definitions for the constructor, accessor and update functions and automatically derives a number of theorems over them (e.g., ``updates on different fields commute'', ``accessors on a record are surjective'', ``accessors yield the value of the last update''). The collection of these theorems constitutes the \<^emph>\memory model\ of Clean, providing an incrementally extensible state-space for global and local program variables. In contrast to axiomatizations of memory models, our generated state-spaces might be ``wrong'' in the sense that they do not reflect the operational behaviour of a particular compiler or a sufficiently large portion of the C language; however, it is by construction \<^emph>\logically consistent\ since it is impossible to derive falsity from the entire set of conservative extension schemes used in their construction. A particular advantage of the incremental state-space construction is that it supports incremental verification and interleaving of program definitions with theory development.\ subsection\ Formally Modeling Control-States \ text\The control state is the ``root'' of all extensions for local and global variable spaces in Clean. It contains just the information of the current control-flow: a \<^term>\break\ occurred (meaning all commands till the end of the control block will be skipped) or a \<^term>\return\ occurred (meaning all commands till the end of the current function body will be skipped).\ record control_state = break_status :: bool return_status :: bool (* ML level representation: *) ML\ val t = @{term "\ \ break_status := False \"}\ (* break quits innermost while or for, return quits an entire execution sequence. *) definition break :: "(unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "break \ (\ \. Some((), \ \ break_status := True \))" definition unset_break_status :: "(unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "unset_break_status \ (\ \. Some((), \ \ break_status := False \))" definition set_return_status :: " (unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "set_return_status = (\ \. Some((), \ \ return_status := True \))" definition unset_return_status :: "(unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "unset_return_status = (\ \. Some((), \ \ return_status := False \))" definition exec_stop :: "('\_ext) control_state_ext \ bool" where "exec_stop = (\ \. break_status \ \ return_status \ )" abbreviation normal_execution :: "('\_ext) control_state_ext \ bool" where "(normal_execution s) \ (\ exec_stop s)" notation normal_execution ("\") lemma exec_stop1[simp] : "break_status \ \ exec_stop \" unfolding exec_stop_def by simp lemma exec_stop2[simp] : "return_status \ \ exec_stop \" unfolding exec_stop_def by simp text\ On the basis of the control-state, assignments, conditionals and loops are reformulated into \<^term>\break\-aware and \<^term>\return\-aware versions as shown in the definitions of \<^term>\assign\ and \<^term>\if_C\ (in this theory file, see below). \ text\For Reasoning over Clean programs, we need the notion of independance of an update from the control-block: \ definition break_status\<^sub>L where "break_status\<^sub>L = create\<^sub>L control_state.break_status control_state.break_status_update" lemma "vwb_lens break_status\<^sub>L" unfolding break_status\<^sub>L_def by (simp add: vwb_lens_def create\<^sub>L_def wb_lens_def mwb_lens_def mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) definition return_status\<^sub>L where "return_status\<^sub>L = create\<^sub>L control_state.return_status control_state.return_status_update" lemma "vwb_lens return_status\<^sub>L" unfolding return_status\<^sub>L_def by (simp add: vwb_lens_def create\<^sub>L_def wb_lens_def mwb_lens_def mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) lemma break_return_indep : "break_status\<^sub>L \ return_status\<^sub>L " by (simp add: break_status\<^sub>L_def lens_indepI return_status\<^sub>L_def upd2put_def create\<^sub>L_def) definition strong_control_independence ("\!") where "\! L = (break_status\<^sub>L \ L \ return_status\<^sub>L \ L)" lemma "vwb_lens break_status\<^sub>L" unfolding vwb_lens_def break_status\<^sub>L_def create\<^sub>L_def wb_lens_def mwb_lens_def by (simp add: mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) definition control_independence :: "(('b\'b)\'a control_state_scheme \ 'a control_state_scheme) \ bool" ("\") where "\ upd \ (\\ T b. break_status (upd T \) = break_status \ \ return_status (upd T \) = return_status \ \ upd T (\\ return_status := b \) = (upd T \)\ return_status := b \ \ upd T (\\ break_status := b \) = (upd T \)\ break_status := b \) " lemma strong_vs_weak_ci : "\! L \ \ (\f. \\. lens_put L \ (f (lens_get L \)))" unfolding strong_control_independence_def control_independence_def by (simp add: break_status\<^sub>L_def lens_indep_def return_status\<^sub>L_def upd2put_def create\<^sub>L_def) lemma expimnt :"\! (create\<^sub>L getv updv) \ (\f \. updv (\_. f (getv \)) \) = updv" unfolding create\<^sub>L_def strong_control_independence_def break_status\<^sub>L_def return_status\<^sub>L_def lens_indep_def apply(rule ext, rule ext) apply auto unfolding upd2put_def (* seems to be independent *) oops lemma expimnt : "vwb_lens (create\<^sub>L getv updv) \ (\f \. updv (\_. f (getv \)) \) = updv" unfolding create\<^sub>L_def strong_control_independence_def lens_indep_def break_status\<^sub>L_def return_status\<^sub>L_def vwb_lens_def apply(rule ext, rule ext) apply auto unfolding upd2put_def wb_lens_def weak_lens_def wb_lens_axioms_def mwb_lens_def mwb_lens_axioms_def apply auto (* seems to be independent *) oops lemma strong_vs_weak_upd : assumes * : "\! (create\<^sub>L getv updv)" (* getv and upd are constructed as lense *) and ** : "(\f \. updv (\_. f (getv \)) \) = updv" (* getv and upd are involutive *) shows "\ (updv)" apply(insert * **) unfolding create\<^sub>L_def upd2put_def by(drule strong_vs_weak_ci, auto) text\This quite tricky proof establishes the fact that the special case \hd(getv \) = []\ for \getv \ = []\ is finally irrelevant in our setting. This implies that we don't need the list-lense-construction (so far).\ lemma strong_vs_weak_upd_list : assumes * : "\! (create\<^sub>L (getv:: 'b control_state_scheme \ 'c list) (updv:: ('c list \ 'c list) \ 'b control_state_scheme \ 'b control_state_scheme))" (* getv and upd are constructed as lense *) and ** : "(\f \. updv (\_. f (getv \)) \) = updv" (* getv and upd are involutive *) shows "\ (updv \ upd_hd)" proof - have *** : "\! (create\<^sub>L (hd \ getv ) (updv \ upd_hd))" using * ** by (simp add: indep_list_lift strong_control_independence_def) show "\ (updv \ upd_hd)" apply(rule strong_vs_weak_upd) apply(rule ***) apply(rule ext, rule ext, simp) apply(subst (2) **[symmetric]) proof - fix f:: "'c \ 'c" fix \ :: "'b control_state_scheme" show "updv (upd_hd (\_. f (hd (getv \)))) \ = updv (\_. upd_hd f (getv \)) \" proof (cases "getv \") case Nil then show ?thesis by (simp,metis (no_types) "**" upd_hd.simps(1)) next case (Cons a list) then show ?thesis proof - have "(\c. f (hd (getv \))) = ((\c. f a)::'c \ 'c)" using local.Cons by auto then show ?thesis by (metis (no_types) "**" local.Cons upd_hd.simps(2)) qed qed qed qed lemma exec_stop_vs_control_independence [simp]: "\ upd \ exec_stop (upd f \) = exec_stop \" unfolding control_independence_def exec_stop_def by simp lemma exec_stop_vs_control_independence' [simp]: "\ upd \ (upd f (\ \ return_status := b \)) = (upd f \)\ return_status := b \" unfolding control_independence_def exec_stop_def by simp lemma exec_stop_vs_control_independence'' [simp]: "\ upd \ (upd f (\ \ break_status := b \)) = (upd f \) \ break_status := b \" unfolding control_independence_def exec_stop_def by simp subsection\An Example for Global Variable Declarations.\ text\We present the above definition of the incremental construction of the state-space in more detail via an example construction. Consider a global variable \A\ representing an array of integer. This \<^emph>\global variable declaration\ corresponds to the effect of the following record declaration: \<^theory_text>\record state0 = control_state + A :: "int list"\ which is later extended by another global variable, say, \B\ representing a real described in the Cauchy Sequence form @{typ "nat \ (int \ int)"} as follows: \<^theory_text>\record state1 = state0 + B :: "nat \ (int \ int)"\. A further extension would be needed if a (potentially recursive) function \f\ with some local variable \tmp\ is defined: \<^theory_text>\record state2 = state1 + tmp :: "nat stack" result_value :: "nat stack" \, where the \stack\ needed for modeling recursive instances is just a synonym for \list\. \ subsection\ The Assignment Operations (embedded in State-Exception Monad) \ text\Based on the global variable states, we define \<^term>\break\-aware and \<^term>\return\-aware version of the assignment. The trick to do this in a generic \<^emph>\and\ type-safe way is to provide the generated accessor and update functions (the ``lens'' representing this global variable, cf. @{cite "Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and "DBLP:conf/ictac/FosterZW16"}) to the generic assign operators. This pair of accessor and update carries all relevant semantic and type information of this particular variable and \<^emph>\characterizes\ this variable semantically. Specific syntactic support~\<^footnote>\via the Isabelle concept of cartouche: \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\\ will hide away the syntactic overhead and permit a human-readable form of assignments or expressions accessing the underlying state. \ consts syntax_assign :: "('\ \ int) \ int \ term" (infix ":=" 60) definition assign :: "(('\_ext) control_state_scheme \ ('\_ext) control_state_scheme) \ (unit,('\_ext) control_state_scheme)MON\<^sub>S\<^sub>E" where "assign f = (\\. if exec_stop \ then Some((), \) else Some((), f \))" definition assign_global :: "(('a \ 'a ) \ '\_ext control_state_scheme \ '\_ext control_state_scheme) \ ('\_ext control_state_scheme \ 'a) \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" (infix ":==\<^sub>G" 100) where "assign_global upd rhs = assign(\\. ((upd) (\_. rhs \)) \)" text\An update of the variable \A\ based on the state of the previous example is done by @{term [source = true] \assign_global A_upd (\\. list_update (A \) (i) (A \ ! j))\} representing \A[i] = A[j]\; arbitrary nested updates can be constructed accordingly.\ text\Local variable spaces work analogously; except that they are represented by a stack in order to support individual instances in case of function recursion. This requires automated generation of specific push- and pop operations used to model the effect of entering or leaving a function block (to be discussed later).\ definition assign_local :: "(('a list \ 'a list) \ '\_ext control_state_scheme \ '\_ext control_state_scheme) \ ('\_ext control_state_scheme \ 'a) \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" (infix ":==\<^sub>L" 100) where "assign_local upd rhs = assign(\\. ((upd o upd_hd) (%_. rhs \)) \)" text\Semantically, the difference between \<^emph>\global\ and \<^emph>\local\ is rather unimpressive as the following lemma shows. However, the distinction matters for the pretty-printing setup of Clean.\ lemma "(upd :==\<^sub>L rhs) = ((upd \ upd_hd) :==\<^sub>G rhs)" unfolding assign_local_def assign_global_def by simp text\The \return\ command in C-like languages is represented basically by an assignment to a local variable \result_value\ (see below in the Clean-package generation), plus some setup of \<^term>\return_status\. Note that a \<^term>\return\ may appear after a \<^term>\break\ and should have no effect in this case.\ definition return\<^sub>C0 where "return\<^sub>C0 A = (\\. if exec_stop \ then Some((), \) else (A ;- set_return_status) \)" definition return\<^sub>C :: "(('a list \ 'a list) \ '\_ext control_state_scheme \ '\_ext control_state_scheme) \ ('\_ext control_state_scheme \ 'a) \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" ("return\") where "return\<^sub>C upd rhs = return\<^sub>C0 (assign_local upd rhs)" subsection\Example for a Local Variable Space\ text\Consider the usual operation \swap\ defined in some free-style syntax as follows: @{cartouche [display] \ function_spec swap (i::nat,j::nat) local_vars tmp :: int defines " \ tmp := A ! i\ ;- \ A[i] := A ! j\ ;- \ A[j] := tmp\ "\} \ text\ For the fantasy syntax \tmp := A ! i\, we can construct the following semantic code: @{term [source = true] \assign_local tmp_update (\\. (A \) ! i )\} where \tmp_update\ is the update operation generated by the \<^theory_text>\record\-package, which is generated while treating local variables of \swap\. By the way, a stack for \return\-values is also generated in order to give semantics to a \return\ operation: it is syntactically equivalent to the assignment of the result variable in the local state (stack). It sets the \<^term>\return_val\ flag. The management of the local state space requires function-specific \push\ and \pop\ operations, for which suitable definitions are generated as well: @{cartouche [display] \definition push_local_swap_state :: "(unit,'a local_swap_state_scheme) MON\<^sub>S\<^sub>E" where "push_local_swap_state \ = Some((),\\local_swap_state.tmp := undefined # local_swap_state.tmp \, local_swap_state.result_value := undefined # local_swap_state.result_value \ \)" definition pop_local_swap_state :: "(unit,'a local_swap_state_scheme) MON\<^sub>S\<^sub>E" where "pop_local_swap_state \ = Some(hd(local_swap_state.result_value \), \\local_swap_state.tmp:= tl( local_swap_state.tmp \) \)"\} where \result_value\ is the stack for potential result values (not needed in the concrete example \swap\). \ section\ Global and Local State Management via Extensible Records \ text\In the sequel, we present the automation of the state-management as schematically discussed in the previous section; the declarations of global and local variable blocks are constructed by subsequent extensions of @{typ "'a control_state_scheme"}, defined above.\ ML\ structure StateMgt_core = struct val control_stateT = Syntax.parse_typ @{context} "control_state" val control_stateS = @{typ "('a)control_state_scheme"}; fun optionT t = Type(@{type_name "Option.option"},[t]); fun MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state)); fun merge_control_stateS (@{typ "('a)control_state_scheme"},t) = t |merge_control_stateS (t, @{typ "('a)control_state_scheme"}) = t |merge_control_stateS (t, t') = if (t = t') then t else error"can not merge Clean state" datatype var_kind = global_var of typ | local_var of typ fun type_of(global_var t) = t | type_of(local_var t) = t type state_field_tab = var_kind Symtab.table structure Data = Generic_Data ( type T = (state_field_tab * typ (* current extensible record *)) val empty = (Symtab.empty,control_stateS) val extend = I fun merge((s1,t1),(s2,t2)) = (Symtab.merge (op =)(s1,s2),merge_control_stateS(t1,t2)) ); val get_data = Data.get o Context.Proof; val map_data = Data.map; val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; val get_state_type = snd o get_data val get_state_type_global = snd o get_data_global val get_state_field_tab = fst o get_data val get_state_field_tab_global = fst o get_data_global fun upd_state_type f = map_data (fn (tab,t) => (tab, f t)) fun upd_state_type_global f = map_data_global (fn (tab,t) => (tab, f t)) fun fetch_state_field (ln,X) = let val a::b:: _ = rev (Long_Name.explode ln) in ((b,a),X) end; fun filter_name name ln = let val ((a,b),X) = fetch_state_field ln in if a = name then SOME((a,b),X) else NONE end; fun filter_attr_of name thy = let val tabs = get_state_field_tab_global thy in map_filter (filter_name name) (Symtab.dest tabs) end; fun is_program_variable name thy = Symtab.defined((fst o get_data_global) thy) name fun is_global_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) name of SOME(global_var _) => true | _ => false fun is_local_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) name of SOME(local_var _) => true | _ => false fun declare_state_variable_global f field thy = let val Const(name,ty) = Syntax.read_term_global thy field in (map_data_global (apfst (Symtab.update_new(name,f ty))) (thy) handle Symtab.DUP _ => error("multiple declaration of global var")) end; fun declare_state_variable_local f field ctxt = let val Const(name,ty) = Syntax.read_term_global (Context.theory_of ctxt) field in (map_data (apfst (Symtab.update_new(name,f ty)))(ctxt) handle Symtab.DUP _ => error("multiple declaration of global var")) end; end\ subsection\Block-Structures\ text\ On the managed local state-spaces, it is now straight-forward to define the semantics for a \block\ representing the necessary management of local variable instances: \ definition block\<^sub>C :: " (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "block\<^sub>C push core pop \ ( \ \assumes break and return unset \ push ;- \ \create new instances of local variables \ core ;- \ \execute the body \ unset_break_status ;- \ \unset a potential break \ unset_return_status;- \ \unset a potential return break \ (x \ pop; \ \restore previous local var instances \ unit\<^sub>S\<^sub>E(x)))" \ \yield the return value \ text\ Based on this definition, the running \swap\ example is represented as follows: @{cartouche [display] \definition swap_core :: "nat \ nat \ (unit,'a local_swap_state_scheme) MON\<^sub>S\<^sub>E" where "swap_core \ (\(i,j). ((assign_local tmp_update (\\. A \ ! i )) ;- (assign_global A_update (\\. list_update (A \) (i) (A \ ! j))) ;- (assign_global A_update (\\. list_update (A \) (j) ((hd o tmp) \)))))" definition swap :: "nat \ nat \ (unit,'a local_swap_state_scheme) MON\<^sub>S\<^sub>E" where "swap \ \(i,j). block\<^sub>C push_local_swap_state (swap_core (i,j)) pop_local_swap_state" \} \ subsection\Call Semantics\ text\It is now straight-forward to define the semantics of a generic call --- which is simply a monad execution that is \<^term>\break\-aware and \<^term>\return\<^bsub>upd\<^esub>\-aware.\ definition call\<^sub>C :: "( '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call\<^sub>C M A\<^sub>1 = (\\. if exec_stop \ then Some(undefined, \) else M (A\<^sub>1 \) \)" text\Note that this presentation assumes a uncurried format of the arguments. The question arises if this is the right approach to handle calls of operation with multiple arguments. Is it better to go for an some appropriate currying principle? Here are some more experimental variants for curried operations... \ definition call_0\<^sub>C :: "('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_0\<^sub>C M = (\\. if exec_stop \ then Some(undefined, \) else M \)" text\The generic version using tuples is identical with @{term \call_1\<^sub>C\}.\ definition call_1\<^sub>C :: "( '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_1\<^sub>C = call\<^sub>C" definition call_2\<^sub>C :: "( '\ \ '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_2\<^sub>C M A\<^sub>1 A\<^sub>2 = (\\. if exec_stop \ then Some(undefined, \) else M (A\<^sub>1 \) (A\<^sub>2 \) \)" definition call_3\<^sub>C :: "( '\ \ '\ \ '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ((('\_ext) control_state_ext) \ '\) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_3\<^sub>C M A\<^sub>1 A\<^sub>2 A\<^sub>3 = (\\. if exec_stop \ then Some(undefined, \) else M (A\<^sub>1 \) (A\<^sub>2 \) (A\<^sub>3 \) \)" (* and 4 and 5 and ... *) section\ Some Term-Coding Functions \ text\In the following, we add a number of advanced HOL-term constructors in the style of @{ML_structure "HOLogic"} from the Isabelle/HOL libraries. They incorporate the construction of types during term construction in a bottom-up manner. Consequently, the leafs of such terms should always be typed, and anonymous loose-@{ML "Bound"} variables avoided.\ ML\ (* HOLogic extended *) fun mk_None ty = let val none = \<^const_name>\Option.option.None\ val none_ty = ty --> Type(\<^type_name>\option\,[ty]) in Const(none, none_ty) end; fun mk_Some t = let val some = \<^const_name>\Option.option.Some\ val ty = fastype_of t val some_ty = ty --> Type(\<^type_name>\option\,[ty]) in Const(some, some_ty) $ t end; fun dest_listTy (Type(\<^type_name>\List.list\, [T])) = T; fun mk_hdT t = let val ty = fastype_of t in Const(\<^const_name>\List.hd\, ty --> (dest_listTy ty)) $ t end fun mk_tlT t = let val ty = fastype_of t in Const(\<^const_name>\List.tl\, ty --> ty) $ t end fun mk_undefined (@{typ "unit"}) = Const (\<^const_name>\Product_Type.Unity\, \<^typ>\unit\) |mk_undefined t = Const (\<^const_name>\HOL.undefined\, t) fun meta_eq_const T = Const (\<^const_name>\Pure.eq\, T --> T --> propT); fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u; fun mk_pat_tupleabs [] t = t | mk_pat_tupleabs [(s,ty)] t = absfree(s,ty)(t) | mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t)); fun read_constname ctxt n = fst(dest_Const(Syntax.read_term ctxt n)) fun wfrecT order recs = let val funT = domain_type (fastype_of recs) val aTy = domain_type funT val ordTy = HOLogic.mk_setT(HOLogic.mk_prodT (aTy,aTy)) in Const(\<^const_name>\Wfrec.wfrec\, ordTy --> (funT --> funT) --> funT) $ order $ recs end fun mk_lens_type from_ty to_ty = Type(@{type_name "lens.lens_ext"}, [from_ty, to_ty, HOLogic.unitT]); \ text\And here comes the core of the \<^theory_text>\Clean\-State-Management: the module that provides the functionality for the commands keywords \<^theory_text>\global_vars\, \<^theory_text>\local_vars\ and \<^theory_text>\local_vars_test\. Note that the difference between \<^theory_text>\local_vars\ and \<^theory_text>\local_vars_test\ is just a technical one: \<^theory_text>\local_vars\ can only be used inside a Clean function specification, made with the \<^theory_text>\function_spec\ command. On the other hand, \<^theory_text>\local_vars_test\ is defined as a global Isar command for test purposes. A particular feature of the local-variable management is the provision of definitions for \<^term>\push\ and \<^term>\pop\ operations --- encoded as \<^typ>\('o, '\) MON\<^sub>S\<^sub>E\ operations --- which are vital for the function specifications defined below. \ ML\ structure StateMgt = struct open StateMgt_core val result_name = "result_value" fun get_result_value_conf name thy = let val S = filter_attr_of name thy in hd(filter (fn ((_,b),_) => b = result_name) S) handle Empty => error "internal error: get_result_value_conf " end; fun mk_lookup_result_value_term name sty thy = let val ((prefix,name),local_var(Type("fun", [_,ty]))) = get_result_value_conf name thy; val long_name = Sign.intern_const thy (prefix^"."^name) val term = Const(long_name, sty --> ty) in mk_hdT (term $ Free("\",sty)) end fun map_to_update sty is_pop thy ((struct_name, attr_name), local_var (Type("fun",[_,ty]))) term = let val tlT = if is_pop then Const(\<^const_name>\List.tl\, ty --> ty) else Const(\<^const_name>\List.Cons\, dest_listTy ty --> ty --> ty) $ mk_undefined (dest_listTy ty) val update_name = Sign.intern_const thy (struct_name^"."^attr_name^"_update") in (Const(update_name, (ty --> ty) --> sty --> sty) $ tlT) $ term end | map_to_update _ _ _ ((_, _),_) _ = error("internal error map_to_update") fun mk_local_state_name binding = Binding.prefix_name "local_" (Binding.suffix_name "_state" binding) fun mk_global_state_name binding = Binding.prefix_name "global_" (Binding.suffix_name "_state" binding) fun construct_update is_pop binding sty thy = let val long_name = Binding.name_of( binding) val attrS = StateMgt_core.filter_attr_of long_name thy in fold (map_to_update sty is_pop thy) (attrS) (Free("\",sty)) end -fun cmd (decl, spec, prems, params) = #2 oo Specification.definition' decl params prems spec +fun cmd (decl, spec, prems, params) = #2 o Specification.definition decl params prems spec fun mk_push_name binding = Binding.prefix_name "push_" binding fun mk_lense_name binding = Binding.suffix_name "\<^sub>L" binding fun push_eq binding name_op rty sty lthy = let val mty = MON_SE_T rty sty val thy = Proof_Context.theory_of lthy val term = construct_update false binding sty thy in mk_meta_eq((Free(name_op, mty) $ Free("\",sty)), mk_Some ( HOLogic.mk_prod (mk_undefined rty,term))) end; fun mk_push_def binding sty lthy = let val name_pushop = mk_push_name binding val rty = \<^typ>\unit\ val eq = push_eq binding (Binding.name_of name_pushop) rty sty lthy val mty = StateMgt_core.MON_SE_T rty sty val args = (SOME(name_pushop, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[]) - in cmd args true lthy end; + in cmd args lthy end; fun mk_pop_name binding = Binding.prefix_name "pop_" binding fun pop_eq binding name_op rty sty lthy = let val mty = MON_SE_T rty sty val thy = Proof_Context.theory_of lthy val res_access = mk_lookup_result_value_term (Binding.name_of binding) sty thy val term = construct_update true binding sty thy in mk_meta_eq((Free(name_op, mty) $ Free("\",sty)), mk_Some ( HOLogic.mk_prod (res_access,term))) end; fun mk_pop_def binding rty sty lthy = let val mty = StateMgt_core.MON_SE_T rty sty val name_op = mk_pop_name binding val eq = pop_eq binding (Binding.name_of name_op) rty sty lthy val args = (SOME(name_op, SOME mty, NoSyn),(Binding.empty_atts,eq),[],[]) - in cmd args true lthy + in cmd args lthy end; fun read_parent NONE ctxt = (NONE, ctxt) | read_parent (SOME raw_T) ctxt = (case Proof_Context.read_typ_abbrev ctxt raw_T of Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); fun read_fields raw_fields ctxt = let val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields); val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts; val ctxt' = fold Variable.declare_typ Ts ctxt; in (fields, ctxt') end; fun parse_typ_'a ctxt binding = let val ty_bind = Binding.prefix_name "'a " (Binding.suffix_name "_scheme" binding) in case Syntax.parse_typ ctxt (Binding.name_of ty_bind) of Type (s, _) => Type (s, [@{typ "'a::type"}]) | _ => error ("Unexpected type" ^ Position.here \<^here>) end fun define_lense binding sty (attr_name,rty,_) lthy = let val prefix = Binding.name_of binding^"_" val name_L = attr_name |> Binding.prefix_name prefix |> mk_lense_name val name_upd = Binding.suffix_name "_update" attr_name val acc_ty = sty --> rty val upd_ty = (rty --> rty) --> sty --> sty val cr = Const(@{const_name "Optics.create\<^sub>L"}, acc_ty --> upd_ty --> mk_lens_type rty sty) val thy = Proof_Context.theory_of lthy val acc_name = Sign.intern_const thy (Binding.name_of attr_name) val upd_name = Sign.intern_const thy (Binding.name_of name_upd) val acc = Const(acc_name, acc_ty) val upd = Const(upd_name, upd_ty) val lens_ty = mk_lens_type rty sty val eq = mk_meta_eq (Free(Binding.name_of name_L, lens_ty), cr $ acc $ upd) val args = (SOME(name_L, SOME lens_ty, NoSyn), (Binding.empty_atts,eq),[],[]) - in cmd args true lthy end + in cmd args lthy end fun add_record_cmd0 read_fields overloaded is_global_kind raw_params binding raw_parent raw_fields thy = let val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; val (parent, ctxt2) = read_parent raw_parent ctxt1; val (fields, ctxt3) = read_fields raw_fields ctxt2; fun lift (a,b,c) = (a, HOLogic.listT b, c) val fields' = if is_global_kind then fields else map lift fields val params' = map (Proof_Context.check_tfree ctxt3) params; val declare = StateMgt_core.declare_state_variable_global fun upd_state_typ thy = let val ctxt = Proof_Context.init_global thy val ty = Syntax.parse_typ ctxt (Binding.name_of binding) in StateMgt_core.upd_state_type_global(K ty)(thy) end fun insert_var ((f,_,_), thy) = if is_global_kind then declare StateMgt_core.global_var (Binding.name_of f) thy else declare StateMgt_core.local_var (Binding.name_of f) thy fun define_push_pop thy = if not is_global_kind then let val sty = parse_typ_'a (Proof_Context.init_global thy) binding; val rty = dest_listTy (#2(hd(rev fields'))) in thy |> Named_Target.theory_map (mk_push_def binding sty) |> Named_Target.theory_map (mk_pop_def binding rty sty) end else thy fun define_lenses thy = let val sty = parse_typ_'a (Proof_Context.init_global thy) binding; in thy |> Named_Target.theory_map (fold (define_lense binding sty) fields') end in thy |> Record.add_record overloaded (params', binding) parent fields' |> (fn thy => List.foldr insert_var (thy) (fields')) |> upd_state_typ |> define_push_pop |> define_lenses end; fun typ_2_string_raw (Type(s,[TFree _])) = if String.isSuffix "_scheme" s then Long_Name.base_name(unsuffix "_scheme" s) else Long_Name.base_name(unsuffix "_ext" s) |typ_2_string_raw (Type(s,_)) = error ("Illegal parameterized state type - not allowed in Clean:" ^ s) |typ_2_string_raw _ = error "Illegal state type - not allowed in Clean." fun new_state_record0 add_record_cmd is_global_kind (((raw_params, binding), res_ty), raw_fields) thy = let val binding = if is_global_kind then mk_global_state_name binding else mk_local_state_name binding val raw_parent = SOME(typ_2_string_raw (StateMgt_core.get_state_type_global thy)) val pos = Binding.pos_of binding fun upd_state_typ thy = StateMgt_core.upd_state_type_global (K (parse_typ_'a (Proof_Context.init_global thy) binding)) thy val result_binding = Binding.make(result_name,pos) val raw_fields' = case res_ty of NONE => raw_fields | SOME res_ty => raw_fields @ [(result_binding,res_ty, NoSyn)] in thy |> add_record_cmd {overloaded = false} is_global_kind raw_params binding raw_parent raw_fields' |> upd_state_typ end val add_record_cmd = add_record_cmd0 read_fields; val add_record_cmd' = add_record_cmd0 pair; val new_state_record = new_state_record0 add_record_cmd val new_state_record' = new_state_record0 add_record_cmd' val _ = Outer_Syntax.command \<^command_keyword>\global_vars\ "define global state record" ((Parse.type_args_constrained -- Parse.binding) -- Scan.succeed NONE -- Scan.repeat1 Parse.const_binding >> (Toplevel.theory o new_state_record true)); ; val _ = Outer_Syntax.command \<^command_keyword>\local_vars_test\ "define local state record" ((Parse.type_args_constrained -- Parse.binding) -- (Parse.typ >> SOME) -- Scan.repeat1 Parse.const_binding >> (Toplevel.theory o new_state_record false)) ; end \ section\Syntactic Sugar supporting \\\-lifting for Global and Local Variables \ ML \ structure Clean_Syntax_Lift = struct type T = { is_local : string -> bool , is_global : string -> bool } val init = Proof_Context.theory_of #> (fn thy => { is_local = fn name => StateMgt_core.is_local_program_variable name thy , is_global = fn name => StateMgt_core.is_global_program_variable name thy }) local fun mk_local_access X = Const (@{const_name "Fun.comp"}, dummyT) $ Const (@{const_name "List.list.hd"}, dummyT) $ X in fun app_sigma0 (st : T) db tm = case tm of Const(name, _) => if #is_global st name then tm $ (Bound db) (* lambda lifting *) else if #is_local st name then (mk_local_access tm) $ (Bound db) (* lambda lifting local *) else tm (* no lifting *) | Free _ => tm | Var _ => tm | Bound n => if n > db then Bound(n + 1) else Bound n | Abs (x, ty, tm') => Abs(x, ty, app_sigma0 st (db+1) tm') | t1 $ t2 => (app_sigma0 st db t1) $ (app_sigma0 st db t2) fun app_sigma db tm = init #> (fn st => app_sigma0 st db tm) fun scope_var st name = if #is_global st name then SOME true else if #is_local st name then SOME false else NONE fun assign_update var = var ^ Record.updateN fun transform_term0 abs scope_var tm = case tm of Const (@{const_name "Clean.syntax_assign"}, _) $ (t1 as Const ("_type_constraint_", _) $ Const (name, ty)) $ t2 => Const ( case scope_var name of SOME true => @{const_name "assign_global"} | SOME false => @{const_name "assign_local"} | NONE => raise TERM ("mk_assign", [t1]) , dummyT) $ Const(assign_update name, ty) $ abs t2 | _ => abs tm fun transform_term st sty = transform_term0 (fn tm => Abs ("\", sty, app_sigma0 st 0 tm)) (scope_var st) fun transform_term' st = transform_term st dummyT fun string_tr ctxt content args = let fun err () = raise TERM ("string_tr", args) in (case args of [(Const (@{syntax_const "_constrain"}, _)) $ (Free (s, _)) $ p] => (case Term_Position.decode_position p of SOME (pos, _) => Symbol_Pos.implode (content (s, pos)) |> Syntax.parse_term ctxt |> transform_term (init ctxt) (StateMgt_core.get_state_type ctxt) |> Syntax.check_term ctxt | NONE => err ()) | _ => err ()) end end end \ syntax "_cartouche_string" :: "cartouche_position \ string" ("_") parse_translation \ [(@{syntax_const "_cartouche_string"}, (fn ctxt => Clean_Syntax_Lift.string_tr ctxt (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] \ section\Support for (direct recursive) Clean Function Specifications \ text\Based on the machinery for the State-Management and implicitly cooperating with the cartouches for assignment syntax, the function-specification \<^theory_text>\function_spec\-package coordinates: \<^enum> the parsing and type-checking of parameters, \<^enum> the parsing and type-checking of pre and post conditions in MOAL notation (using \\\-lifting cartouches and implicit reference to parameters, pre and post states), \<^enum> the parsing local variable section with the local-variable space generation, \<^enum> the parsing of the body in this extended variable space, \<^enum> and optionally the support of measures for recursion proofs. The reader interested in details is referred to the \<^file>\../examples/Quicksort_concept.thy\-example, accompanying this distribution. \ text\In order to support the \<^verbatim>\old\-notation known from JML and similar annotation languages, we introduce the following definition:\ definition old :: "'a \ 'a" where "old x = x" text\The core module of the parser and operation specification construct is implemented in the following module:\ ML \ structure Function_Specification_Parser = struct type funct_spec_src = { binding: binding, (* name *) params: (binding*string) list, (* parameters and their type*) ret_type: string, (* return type; default unit *) locals: (binding*string*mixfix)list, (* local variables *) pre_src: string, (* precondition src *) post_src: string, (* postcondition src *) variant_src: string option, (* variant src *) body_src: string * Position.T (* body src *) } type funct_spec_sem_old = { params: (binding*typ) list, (* parameters and their type*) ret_ty: typ, (* return type *) pre: term, (* precondition *) post: term, (* postcondition *) variant: term option (* variant *) } type funct_spec_sem = { binding: binding, (* name *) params: (binding*string) list, (* parameters and their type*) ret_type: string, (* return type; default unit *) locals: (binding*string*mixfix)list, (* local variables *) read_pre: Proof.context -> term, (* precondition src *) read_post: Proof.context -> term, (* postcondition src *) read_variant_opt: (Proof.context->term) option, (* variant src *) read_body: Proof.context -> typ -> term (* body src *) } val parse_arg_decl = Parse.binding -- (Parse.$$$ "::" |-- Parse.typ) val parse_param_decls = Args.parens (Parse.enum "," parse_arg_decl) val parse_returns_clause = Scan.optional (\<^keyword>\returns\ |-- Parse.typ) "unit" val locals_clause = (Scan.optional ( \<^keyword>\local_vars\ -- (Scan.repeat1 Parse.const_binding)) ("", [])) val parse_proc_spec = ( Parse.binding -- parse_param_decls -- parse_returns_clause --| \<^keyword>\pre\ -- Parse.term --| \<^keyword>\post\ -- Parse.term -- (Scan.option ( \<^keyword>\variant\ |-- Parse.term)) -- (Scan.optional( \<^keyword>\local_vars\ |-- (Scan.repeat1 Parse.const_binding))([])) --| \<^keyword>\defines\ -- (Parse.position (Parse.term)) ) >> (fn ((((((((binding,params),ret_ty),pre_src),post_src),variant_src),locals)),body_src) => { binding = binding, params=params, ret_type=ret_ty, pre_src=pre_src, post_src=post_src, variant_src=variant_src, locals=locals, body_src=body_src} : funct_spec_src ) fun read_params params ctxt = let val Ts = Syntax.read_typs ctxt (map snd params); in (Ts, fold Variable.declare_typ Ts ctxt) end; fun read_result ret_ty ctxt = let val [ty] = Syntax.read_typs ctxt [ret_ty] val ctxt' = Variable.declare_typ ty ctxt in (ty, ctxt') end fun read_function_spec ( params, ret_type, read_variant_opt) ctxt = let val (params_Ts, ctxt') = read_params params ctxt val (rty, ctxt'') = read_result ret_type ctxt' val variant = case read_variant_opt of NONE => NONE |SOME f => SOME(f ctxt'') val paramT_l = (map2 (fn (b, _) => fn T => (b, T)) params params_Ts) in ((paramT_l, rty, variant),ctxt'') end fun check_absence_old term = let fun test (s,ty) = if s = @{const_name "old"} andalso fst (dest_Type ty) = "fun" then error("the old notation is not allowed here!") else false in exists_Const test term end fun transform_old sty term = let fun transform_old0 (Const(@{const_name "old"}, Type ("fun", [_,_])) $ term ) = (case term of (Const(s,ty) $ Bound x) => (Const(s,ty) $ Bound (x+1)) | _ => error("illegal application of the old notation.")) |transform_old0 (t1 $ t2) = transform_old0 t1 $ transform_old0 t2 |transform_old0 (Abs(s,ty,term)) = Abs(s,ty,transform_old0 term) |transform_old0 term = term in Abs("\\<^sub>p\<^sub>r\<^sub>e", sty, transform_old0 term) end fun define_cond binding f_sty transform_old check_absence_old cond_suffix params read_cond (ctxt:local_theory) = let val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params val src' = case transform_old (read_cond ctxt) of Abs(nn, sty_pre, term) => mk_pat_tupleabs params' (Abs(nn,sty_pre,term)) | _ => error ("define abstraction for result" ^ Position.here \<^here>) val bdg = Binding.suffix_name cond_suffix binding val _ = check_absence_old src' val bdg_ty = HOLogic.mk_tupleT(map (#2) params) --> f_sty HOLogic.boolT val eq = mk_meta_eq(Free(Binding.name_of bdg, bdg_ty),src') val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) - in StateMgt.cmd args true ctxt end + in StateMgt.cmd args ctxt end fun define_precond binding sty = define_cond binding (fn boolT => sty --> boolT) I check_absence_old "_pre" fun define_postcond binding rty sty = define_cond binding (fn boolT => sty --> sty --> rty --> boolT) (transform_old sty) I "_post" fun define_body_core binding args_ty sty params body = let val params' = map (fn(b,ty) => (Binding.name_of b, ty)) params val bdg_core = Binding.suffix_name "_core" binding val bdg_core_name = Binding.name_of bdg_core val umty = args_ty --> StateMgt.MON_SE_T @{typ "unit"} sty val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs params' body) val args_core =(SOME (bdg_core, SOME umty, NoSyn), (Binding.empty_atts, eq), [], []) - in StateMgt.cmd args_core true + in StateMgt.cmd args_core end fun define_body_main {recursive = x:bool} binding rty sty params read_variant_opt _ ctxt = let val push_name = StateMgt.mk_push_name (StateMgt.mk_local_state_name binding) val pop_name = StateMgt.mk_pop_name (StateMgt.mk_local_state_name binding) val bdg_core = Binding.suffix_name "_core" binding val bdg_core_name = Binding.name_of bdg_core val bdg_rec_name = Binding.name_of(Binding.suffix_name "_rec" binding) val bdg_ord_name = Binding.name_of(Binding.suffix_name "_order" binding) val args_ty = HOLogic.mk_tupleT (map snd params) val rmty = StateMgt_core.MON_SE_T rty sty val umty = StateMgt.MON_SE_T @{typ "unit"} sty val argsProdT = HOLogic.mk_prodT(args_ty,args_ty) val argsRelSet = HOLogic.mk_setT argsProdT val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params val measure_term = case read_variant_opt of NONE => Free(bdg_ord_name,args_ty --> HOLogic.natT) | SOME f => ((f ctxt) |> mk_pat_tupleabs params') val measure = Const(@{const_name "Wellfounded.measure"}, (args_ty --> HOLogic.natT) --> argsRelSet ) $ measure_term val lhs_main = if x andalso is_none (read_variant_opt ) then Free(Binding.name_of binding, (args_ty --> HOLogic.natT) --> args_ty --> rmty) $ Free(bdg_ord_name, args_ty --> HOLogic.natT) else Free(Binding.name_of binding, args_ty --> rmty) val rhs_main = mk_pat_tupleabs params' (Const(@{const_name "Clean.block\<^sub>C"}, umty --> umty --> rmty --> rmty) $ Const(read_constname ctxt (Binding.name_of push_name),umty) $ (Const(read_constname ctxt bdg_core_name, args_ty --> umty) $ HOLogic.mk_tuple (map Free params')) $ Const(read_constname ctxt (Binding.name_of pop_name),rmty)) val rhs_main_rec = wfrecT measure (Abs(bdg_rec_name, (args_ty --> umty) , mk_pat_tupleabs params' (Const(@{const_name "Clean.block\<^sub>C"}, umty-->umty-->rmty-->rmty) $ Const(read_constname ctxt (Binding.name_of push_name),umty) $ (Const(read_constname ctxt bdg_core_name, (args_ty --> umty) --> args_ty --> umty) $ (Bound (length params)) $ HOLogic.mk_tuple (map Free params')) $ Const(read_constname ctxt (Binding.name_of pop_name),rmty)))) val eq_main = mk_meta_eq(lhs_main, if x then rhs_main_rec else rhs_main ) val args_main = (SOME(binding,NONE,NoSyn), (Binding.empty_atts,eq_main),[],[]) - in ctxt |> StateMgt.cmd args_main true + in ctxt |> StateMgt.cmd args_main end val _ = Local_Theory.exit_result_global; val _ = Named_Target.theory_map_result; val _ = Named_Target.theory_map; (* This code is in large parts so messy because the extensible record package (used inside StateMgt.new_state_record) is only available as transformation on global contexts, which cuts the local context calculations into two halves. The second halves is cut again into two halves because the definition of the core apparently does not take effect before defining the block - structure when not separated (this problem can perhaps be overcome somehow)) Precondition: the terms of the read-functions are full typed in the respective local contexts. *) fun checkNsem_function_spec_gen {recursive = false} ({read_variant_opt=SOME _, ...}) _ = error "No measure required in non-recursive call" |checkNsem_function_spec_gen (isrec as {recursive = _:bool}) ({binding, ret_type, read_variant_opt, locals, read_body, read_pre, read_post, params} : funct_spec_sem) thy = let fun addfixes ((params_Ts,ret_ty,t_opt), ctxt) = (fn fg => fn ctxt => ctxt |> Proof_Context.add_fixes (map (fn (s,ty)=>(s,SOME ty,NoSyn)) params_Ts) (* this declares the parameters of a function specification as Free variables (overrides a possible constant declaration) and assigns the declared type to them *) |> (fn (X, ctxt) => fg params_Ts ret_ty ctxt) , ctxt) val (theory_map, thy') = Named_Target.theory_map_result (K (fn f => Named_Target.theory_map o f)) ( read_function_spec (params, ret_type, read_variant_opt) #> addfixes ) (thy) in thy' |> theory_map let val sty_old = StateMgt_core.get_state_type_global thy' fun parse_contract params ret_ty = ( define_precond binding sty_old params read_pre #> define_postcond binding ret_ty sty_old params read_post) in parse_contract end |> StateMgt.new_state_record false ((([],binding), SOME ret_type),locals) |> theory_map (fn params => fn ret_ty => fn ctxt => let val sty = StateMgt_core.get_state_type ctxt val args_ty = HOLogic.mk_tupleT (map snd params) val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty val body = read_body ctxt mon_se_ty val ctxt' = if #recursive isrec then Proof_Context.add_fixes [(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2 else ctxt val body = read_body ctxt' mon_se_ty in ctxt' |> define_body_core binding args_ty sty params body end) (* separation nasty, but nec. in order to make the body definition take effect. No other reason. *) |> theory_map (fn params => fn ret_ty => fn ctxt => let val sty = StateMgt_core.get_state_type ctxt val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty val body = read_body ctxt mon_se_ty in ctxt |> define_body_main isrec binding ret_ty sty params read_variant_opt body end) end fun checkNsem_function_spec (isrec as {recursive = _:bool}) ( {binding, ret_type, variant_src, locals, body_src, pre_src, post_src, params} : funct_spec_src) thy = checkNsem_function_spec_gen (isrec) ( {binding = binding, params = params, ret_type = ret_type, read_variant_opt = (case variant_src of NONE => NONE | SOME t=> SOME(fn ctxt => Syntax.read_term ctxt t)), locals = locals, read_body = fn ctxt => fn expected_type => Syntax.read_term ctxt (fst body_src), read_pre = fn ctxt => Syntax.read_term ctxt pre_src, read_post = fn ctxt => Syntax.read_term ctxt post_src} : funct_spec_sem) thy val _ = Outer_Syntax.command \<^command_keyword>\function_spec\ "define Clean function specification" (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = false})); val _ = Outer_Syntax.command \<^command_keyword>\rec_function_spec\ "define recursive Clean function specification" (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = true})); end \ section\The Rest of Clean: Break/Return aware Version of If, While, etc.\ definition if_C :: "[('\_ext) control_state_ext \ bool, ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E, ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E] \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "if_C c E F = (\\. if exec_stop \ then Some(undefined, \) \ \state unchanged, return arbitrary\ else if c \ then E \ else F \)" syntax (xsymbols) "_if_SECLEAN" :: "['\ \ bool,('o,'\)MON\<^sub>S\<^sub>E,('o','\)MON\<^sub>S\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>E" ("(if\<^sub>C _ then _ else _fi)" [5,8,8]20) translations "(if\<^sub>C cond then T1 else T2 fi)" == "CONST Clean.if_C cond T1 T2" definition while_C :: "(('\_ext) control_state_ext \ bool) \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "while_C c B \ (\\. if exec_stop \ then Some((), \) else ((MonadSE.while_SE (\ \. \exec_stop \ \ c \) B) ;- unset_break_status) \)" syntax (xsymbols) "_while_C" :: "['\ \ bool, (unit, '\)MON\<^sub>S\<^sub>E] \ (unit, '\)MON\<^sub>S\<^sub>E" ("(while\<^sub>C _ do _ od)" [8,8]20) translations "while\<^sub>C c do b od" == "CONST Clean.while_C c b" section\Miscellaneous\ text\Since \<^verbatim>\int\ were mapped to Isabelle/HOL @{typ "int"} and \<^verbatim>\unsigned int\ to @{typ "nat"}, there is the need for a common interface for accesses in arrays, which were represented by Isabelle/HOL lists: \ consts nth\<^sub>C :: "'a list \ 'b \ 'a" overloading nth\<^sub>C \ "nth\<^sub>C :: 'a list \ nat \ 'a" begin definition nth\<^sub>C_nat : "nth\<^sub>C (S::'a list) (a) \ nth S a" end overloading nth\<^sub>C \ "nth\<^sub>C :: 'a list \ int \ 'a" begin definition nth\<^sub>C_int : "nth\<^sub>C (S::'a list) (a) \ nth S (nat a)" end definition while_C_A :: " (('\_ext) control_state_scheme \ bool) \ (('\_ext) control_state_scheme \ nat) \ (('\_ext) control_state_ext \ bool) \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "while_C_A Inv f c B \ while_C c B" ML\ structure Clean_Term_interface = struct fun mk_seq_C C C' = let val t = fastype_of C val t' = fastype_of C' in Const(\<^const_name>\bind_SE'\, t --> t' --> t') end; fun mk_skip_C sty = Const(\<^const_name>\skip\<^sub>S\<^sub>E\, StateMgt_core.MON_SE_T HOLogic.unitT sty) fun mk_break sty = Const(\<^const_name>\if_C\, StateMgt_core.MON_SE_T HOLogic.unitT sty ) fun mk_return_C upd rhs = let val ty = fastype_of rhs val (sty,rty) = case ty of Type("fun", [sty,rty]) => (sty,rty) | _ => error "mk_return_C: illegal type for body" val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty val rhs_ty = sty --> rty val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty in Const(\<^const_name>\return\<^sub>C\, upd_ty --> rhs_ty --> mty) $ upd $ rhs end fun mk_assign_global_C upd rhs = let val ty = fastype_of rhs val (sty,rty) = case ty of Type("fun", [sty,rty]) => (sty,rty) | _ => error "mk_assign_global_C: illegal type for body" val upd_ty = (rty --> rty) --> sty --> sty val rhs_ty = sty --> rty val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty in Const(\<^const_name>\assign_global\, upd_ty --> rhs_ty --> mty) $ upd $ rhs end fun mk_assign_local_C upd rhs = let val ty = fastype_of rhs val (sty,rty) = case ty of Type("fun", [sty,rty]) => (sty,rty) | _ => error "mk_assign_local_C: illegal type for body" val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty val rhs_ty = sty --> rty val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty in Const(\<^const_name>\assign_local\, upd_ty --> rhs_ty --> mty) $ upd $ rhs end fun mk_call_C opn args = let val ty = fastype_of opn val (argty,mty) = case ty of Type("fun", [argty,mty]) => (argty,mty) | _ => error "mk_call_C: illegal type for body" val sty = case mty of Type("fun", [sty,_]) => sty | _ => error "mk_call_C: illegal type for body 2" val args_ty = sty --> argty in Const(\<^const_name>\call\<^sub>C\, ty --> args_ty --> mty) $ opn $ args end (* missing : a call_assign_local and a call_assign_global. Or define at HOL level ? *) fun mk_if_C c B B' = let val ty = fastype_of B val ty_cond = case ty of Type("fun", [argty,_]) => argty --> HOLogic.boolT |_ => error "mk_if_C: illegal type for body" in Const(\<^const_name>\if_C\, ty_cond --> ty --> ty --> ty) $ c $ B $ B' end; fun mk_while_C c B = let val ty = fastype_of B val ty_cond = case ty of Type("fun", [argty,_]) => argty --> HOLogic.boolT |_ => error "mk_while_C: illegal type for body" in Const(\<^const_name>\while_C\, ty_cond --> ty --> ty) $ c $ B end; fun mk_while_anno_C inv f c B = (* no type-check on inv and measure f *) let val ty = fastype_of B val (ty_cond,ty_m) = case ty of Type("fun", [argty,_]) =>( argty --> HOLogic.boolT, argty --> HOLogic.natT) |_ => error "mk_while_anno_C: illegal type for body" in Const(\<^const_name>\while_C_A\, ty_cond --> ty_m --> ty_cond --> ty --> ty) $ inv $ f $ c $ B end; fun mk_block_C push body pop = let val body_ty = fastype_of body val pop_ty = fastype_of pop val bty = body_ty --> body_ty --> pop_ty --> pop_ty in Const(\<^const_name>\block\<^sub>C\, bty) $ push $ body $ pop end end;\ section\Function-calls in Expressions\ text\The precise semantics of function-calls appearing inside expressions is underspecified in C, which is a notorious problem for compilers and analysis tools. In Clean, it is impossible by construction --- and the type displine --- to have function-calls inside expressions. However, there is a somewhat \<^emph>\recommended coding-scheme\ for this feature, which leaves this issue to decisions in the front-end: \begin{verbatim} a = f() + g(); \end{verbatim} can be represented in Clean by: \x \ f(); y \ g(); \a := x + y\ \ or \x \ g(); y \ f(); \a := y + x\ \ which makes the evaluation order explicit without introducing local variables or any form of explicit trace on the state-space of the Clean program. We assume, however, even in this coding scheme, that \<^verbatim>\f()\ and \<^verbatim>\g()\ are atomic actions; note that this assumption is not necessarily justified in modern compilers, where actually neither of these two (atomic) serializations of \<^verbatim>\f()\ and \<^verbatim>\g()\ may exists. Note, furthermore, that expressions may not only be right-hand-sides of (local or global) assignments or conceptually similar return-statements, but also passed as argument of other function calls, where the same problem arises. \ end