| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Clean/src/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 82 kB |
|
Quelle Clean.thySprache: Isabelle |
|||||||||||||||
|
(****************************************************************************** * 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 i C-like control-flow operators based on a shallow embedding into the ``State Exc in 🍋‹MonadSE.thy›. It strives for a type-safe notation of program-variables, a construction of the typed state-space in order to facilitate incremental verifi open-world extensibility to new type definitions intertwined with the program . 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 loca end{itemize} that Clean in its current version is restricted to 🪙‹monomorphic› global and l well as function parameters. This limitation will be overcome at a later stage. itself, however, is deeply based on parametric polymorphism (enabling structure records as used in languages of the ML family 🪙‹http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/21num.pdf› Haskell 🪙‹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 🪙‹type_synonym ('o, 'σ) MONSE = ‹'σ ⇀ ('o × 'σ)›› with the definitions of term‹bind› and term‹unit›. this language, sequence operators, conditionals and loops can be integrated. › text‹From a concrete program, the underlying state 🪙‹'σ› is 🪙‹incrementally› co of extensible record definitions: 🪙 Initially, an internal control state is defined to give semantics to term‹bre term‹return› statements: \begin{isar} record control_state = break_val :: bool return_val :: bool \end{isar} 🪙‹control_state› represents the $\sigma_0$ state. 🪙 Any global variable definition block with definitions $a_1 : \tau_1$ $\dots$ is translated into a record extension: \begin{isar} record σ$_{n+1}$ = σ$_n$ + a$_1$ :: $\tau_1$; ...; $a_n$ :: $\tau_n$ \end{isar} 🪙 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 re \begin{isar} record σ$_{n+1}$ = σ$_n$ + a$_1$ :: $\tau_1$ list; ...; $a_n$ :: $\tau_n$ li \end{isar} where the 🍋‹_ list›-lifting is used to model a 🪙‹stack› of local variable inst in case of direct recursions and the term‹result_value› used for the value of th statement. text ‹ The 🪙‹record› package creates an 🪙‹'σ› extensible record type 🪙‹'σ control_state_ext› where the 🪙‹'σ› stands for extensions that are subsequen . Furthermore, it generates definitions for the constructor, accessor and update derives a number of theorems over them (e.g., ``updates on different fields com `accessors on a record are surjective'', ``accessors yield the value of the last of these theorems constitutes the 🪙‹memory model› of Clean, providing an incre state-space for global and local program variables. In contrast to axiomatizati memory models, our generated state-spaces might be ``wrong'' in the sense that the operational behaviour of a particular compiler or a sufficiently large port language; however, it is by construction 🪙‹logically consistent› since it is to derive falsity from the entire set of conservative extension schemes used in . A particular advantage of the incremental state-space construction is that it incremental verification and interleaving of program definitions with theory de subsection‹ Formally Modeling Control-States › text‹The control state is the ``root'' of all extensions for local and global va in Clean. It contains just the information of the current control-flow: a term‹ meaning all commands till the end of the control block will be skipped) or a ter 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) MONSE" where "break ≡ (λ σ. Some((), σ ( break_status := True )))" definition unset_break_status :: "(unit, ('σ_ext) control_state_ext) MONSE" where "unset_break_status ≡ (λ σ. Some((), σ ( break_status := False )))" definition set_return_status :: " (unit, ('σ_ext) control_state_ext) MONSE" where "set_return_status = (λ σ. Some((), σ ( return_status := True )))" definition unset_return_status :: "(unit, ('σ_ext) control_state_ext) MONSE" 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 into term‹break›-aware and term‹return›-aware versions as shown in the definitio 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_statusL where "break_statusL = createL control_state.break_status control_state.break_sta lemma "vwb_lens break_statusL" unfolding break_statusL_def by (simp add: vwb_lens_def createL_def wb_lens_def mwb_lens_def mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) definition return_statusL where "return_statusL = createL control_state.return_status control_state.return_ lemma "vwb_lens return_statusL" unfolding return_statusL_def by (simp add: vwb_lens_def createL_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_statusL ⋈ return_statusL " by (simp add: break_statusL_def lens_indepI return_statusL_def upd2put_def createL_def) definition strong_control_independence (‹♯!›) where "♯! L = (break_statusL ⋈ L ∧ return_statusL ⋈ L)" lemma "vwb_lens break_statusL" unfolding vwb_lens_def break_statusL_def createL_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_statusL_def lens_indep_def return_statusL_def upd2put_def createL_d lemma expimnt :"♯! (createL getv updv) ==> (λf σ. updv (λ_. f (getv σ)) σ) = updv" unfolding createL_def strong_control_independence_def break_statusL_def return_statusL_def lens_indep_def apply(rule ext, rule ext) apply auto unfolding upd2put_def (* seems to be independent *) oops lemma expimnt : "vwb_lens (createL getv updv) ==> (λf σ. updv (λ_. f (getv σ)) σ) = updv" unfolding createL_def strong_control_independence_def lens_indep_def break_statusL_def return_statusL_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 * : "♯! (createL 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 createL_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 * : "♯! (createL (getv:: 'b control_state_scheme ==> 'c list) (updv:: ('c list ==> 'c list) ==> 'b control_state_scheme ==> 'b control_state_s (* getv and upd are constructed as lense *) and ** : "(λf σ. updv (λ_. f (getv σ)) σ) = updv" (* getv and upd are involutive *) shows "♯ (updv ∘ upd_hd)" proof - have *** : "♯! (createL (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 stat via an example construction. a global variable ‹A› representing an array of integer. This 🪙‹global variable declaration› corresponds to the effect of the following declaration: 🪙‹record state0 = control_state + A :: "int list"› is later extended by another global variable, say, ‹B› representing a real in the Cauchy Sequence form @{typ "nat ==> (int × int)"} as follows: 🪙‹record state1 = state0 + B :: "nat ==> (int × int)"›. further extension would be needed if a (potentially recursive) function ‹f› wit ‹tmp› is defined: 🪙‹record state2 = state1 + tmp :: "nat stack" result_value :: "nat stack" ›, wh 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 of the assignment. The trick to do this in a generic 🪙‹and› type-safe way is t generated accessor and update functions (the ``lens'' representing this global . cite‹"Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and DBLP:conf/ictac/FosterZW16"›) to the generic assign operators. This pair of acce all relevant semantic and type information of this particular variable and 🪙‹c variable semantically. Specific syntactic support~🪙‹via the Isabelle concept o : 🪙‹https://isabelle.in.tum.de/doc/isar-ref.pdf› permit a human-readable form of assignments or expressions accessing the underl consts syntax_assign :: "('α ==> int) ==> int ==> term" (infix ‹:=› 60) definition assign :: "(('σ_ext) control_state_scheme ==> ('σ_ext) control_state_scheme) ==> (unit,('σ_ext) control_state_scheme)MONSE" where "assign f = (λσ. if exec_stop σ then Some((), σ) else Some((), f σ))" definition assign_global :: "(('a ==> 'a ) ==> 'σ_ext control_state_scheme ==> 'σ_ex ==> ('σ_ext control_state_scheme ==> 'a) ==> (unit,'σ_ext control_state_scheme) MONSE" (infix ‹:==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 @{term [source = true] ‹assign_global A_upd (λσ. list_update (A σ) (i) (A σ ! j))›} ‹A[i] = A[j]›; arbitrary nested updates can be constructed accordingly. text‹Local variable spaces work analogously; except that they are represented by order to support individual instances in case of function recursion. This requi generation of specific push- and pop operations used to model the effect of 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) MONSE" (infix ‹:==L› 100) where "assign_local upd rhs = assign(λσ. ((upd o upd_hd) (%_. rhs σ)) σ)" text‹Semantically, the difference between 🪙‹global› and 🪙‹local› is rather uni following lemma shows. However, the distinction matters for the pretty-printing lemma "(upd :==L rhs) = ((upd ∘ upd_hd) :==G rhs)" unfolding assign_local_def assign_global_def by simp text‹The ‹return› command in C-like languages is represented basically by an ass ‹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 this case. definition returnC0 where "returnC0 A = (λσ. if exec_stop σ then Some((), σ) else (A ;- set_return_status) σ)" definition returnC :: "(('a list ==> 'a list) ==> 'σ_ext control_state_scheme ==> 'σ_ ==> ('σ_ext control_state_scheme ==> 'a) ==> (unit,'σ_ext control_state_scheme) MONSE" (‹return🍋›) where "returnC upd rhs = returnC0 (assign_local upd rhs)" subsection‹Example for a Local Variable Space› text‹Consider the usual operation ‹swap› defined in some free-style syntax as fo {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‹ the fantasy syntax ‹tmp := A ! i›, we can construct the following semantic cod {term [source = true] ‹assign_local tmp_update (λσ. (A σ) ! i )›} where ‹tmp_update operation generated by the 🪙‹record›-package, which is generated while treatin ‹swap›. By the way, a stack for ‹return›-values is also generated in order to g a ‹return› operation: it is syntactically equivalent to the assignment of result variable in the local state (stack). It sets the term‹return_val› flag. management of the local state space requires function-specific ‹push› and ‹pop› which suitable definitions are generated as well: {cartouche [display] ‹definition push_local_swap_state :: "(unit,'a local_swap_state_scheme) MONSE" 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) MONSE" where "pop_local_swap_state σ = Some(hd(local_swap_state.result_value σ), σ(local_swap_state.tmp:= tl( local_swap_state.tmp σ) ))"›} ‹result_value› is the stack for potential result values (not needed in the conc ‹swap›). section‹ Global and Local State Management via Extensible Records › text‹In the sequel, we present the automation of the state-management as schemat the previous section; the declarations of global and local variable blocks are extensions of @{typ "'a control_state_scheme"}, defined above. ML‹ StateMgt_core = control_stateT = Syntax.parse_typ @{context} "control_state" control_stateS = @{typ "('a)control_state_scheme"}; optionT t = Type(@{type_name "Option.option"},[t]); MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state)); 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 Clea var_kind = global_var of typ | local_var of typ type_of(global_var t) = t | type_of(local_var t) = t state_field_tab = var_kind Symtab.table 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) SOME(global_var _) => true | _ => false fun is_local_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) n 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\<open> On the managed local state-spaces, it is now straight-forward to define the semanti a \<open>block\<close> representing the necessary management of local variable instances: \<close> definition block\<^sub>C :: " (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E \<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E \<Rightarrow> ('\<alpha>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E \<Rightarrow> ('\<alpha>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "block\<^sub>C push core pop \<equiv> ( \<comment> \<open>assumes break and return unset \<close> push ;- \<comment> \<open>create new instances of local variables \<close> core ;- \<comment> \<open>execute the body \<close> unset_break_status ;- \<comment> \<open>unset a potential break \<close> unset_return_status;- \<comment> \<open>unset a potential return break \<close> (x \<leftarrow> pop; \<comment> \<open>restore previous local var instances \<close> unit\<^sub>S\<^sub>E(x)))" \<comment> \<open>yield the return value \<close> text\<open> Based on this definition, the running \<open>swap\<close> example is represented as fo @{cartouche [display] \<open>definition swap_core :: "nat \<times> nat \<Rightarrow> (unit,'a local_swap_state_schem where "swap_core \<equiv> (\<lambda>(i,j). ((assign_local tmp_update (\<lambda>\<sigma>. A \<sigm (assign_global A_update (\<lambda>\<sigma>. list_update (A \<sigma>) (i) (A \<sigma> ! j))) ;- (assign_global A_update (\<lambda>\<sigma>. list_update (A \<sigma>) (j) ((hd o tmp) \<sigma>))))) definition swap :: "nat \<times> nat \<Rightarrow> (unit,'a local_swap_state_scheme) MON\<^sub> where "swap \<equiv> \<lambda>(i,j). block\<^sub>C push_local_swap_state (swap_core (i,j)) pop \<close>} \<close> subsection\<open>Call Semantics\<close> text\<open>It is now straight-forward to define the semantics of a generic call --- which is simply a monad execution that is \<^term>\<open>break\<close>-aware and \<^term>\<open>retu definition call\<^sub>C :: "( '\<alpha> \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext) ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<alpha>) \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call\<^sub>C M A\<^sub>1 = (\<lambda>\<sigma>. if exec_stop \<sigma> then Some(undefined, \<sig text\<open>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 argume Is it better to go for an some appropriate currying principle? Here are some more experimental variants for curried operations... \<close> definition call_0\<^sub>C :: "('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E \<R where "call_0\<^sub>C M = (\<lambda>\<sigma>. if exec_stop \<sigma> then Some(undefined, \<sigma>) el text\<open>The generic version using tuples is identical with @{term \<open>call_1\<^sub>C\<clos definition call_1\<^sub>C :: "( '\<alpha> \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ex ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<alpha>) \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_1\<^sub>C = call\<^sub>C" definition call_2\<^sub>C :: "( '\<alpha> \<Rightarrow> '\<beta> \<Rightarrow> ('\<rho>, ('\<sigma>_ext ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<alpha>) \<Rightarrow> ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<beta>) \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_2\<^sub>C M A\<^sub>1 A\<^sub>2 = (\<lambda>\<sigma>. if exec_stop \<sigma> then Some(undef definition call_3\<^sub>C :: "( '\<alpha> \<Rightarrow> '\<beta> \<Rightarrow> '\<gamma> \<Rightarrow> ( ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<alpha>) \<Rightarrow> ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<beta>) \<Rightarrow> ((('\<sigma>_ext) control_state_ext) \<Rightarrow> '\<gamma>) \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_3\<^sub>C M A\<^sub>1 A\<^sub>2 A\<^sub>3 = (\<lambda>\<sigma>. if exec_stop \<sigma> then Som else M (A\<^sub>1 \<sigma>) (A\<^sub>2 \<sigma>) (A\<^sub>3 \<sigma>) \<sigma>)" (* 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 {ML_structure "HOLogic"} from the Isabelle/HOL libraries. They incorporate the c types during term construction in a bottom-up manner. Consequently, the leafs o should always be typed, and anonymous loose-@{ML "Bound"} variables avoided. ML‹ (* HOLogic extended *) fun mk_None ty = let val none = 🍋‹Option.option.None› val none_ty = ty --> Type(🍋‹option›,[ty]) in Const(none, none_ty) end; fun mk_Some t = let val some = 🍋‹Option.option.Some› val ty = fastype_of t val some_ty = ty --> Type(🍋‹option›,[ty]) in Const(some, some_ty) $ t end; fun dest_listTy (Type(🍋‹List.list›, [T])) = T; fun is_listTy t = case t of (Type(🍋‹List.list›, [T])) => true | _ => false fun mk_hdT t = let val ty = fastype_of t in Const(🍋‹List.hd›, ty --> (dest_listTy ty)) $ t end fun mk_tlT t = let val ty = fastype_of t in Const(🍋‹List.tl›, ty --> ty) $ t end fun mk_undefined (@{typ "unit"}) = Const (🍋‹Product_Type.Unity›, 🍋‹unit›) |mk_undefined t = Const (🍋‹HOL.undefined›, t) fun meta_eq_const T = Const (🍋‹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 fun mk_pat_tupleabs_wrapper [] t = absfree("unitparam",@{typ unit}) t | mk_pat_tupleabs_wrapper R t = 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(🍋‹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 🪙‹Clean›-State-Management: the module that prov functionality for the commands keywords 🪙‹global_vars›, 🪙‹local_vars› and 🪙‹local_va Note that the difference between 🪙‹local_vars› and 🪙‹local_vars_test› is just a technic 🪙‹local_vars› can only be used inside a Clean function specification, made with the 🪙‹func command. On the other hand, 🪙‹local_vars_test› is defined as a global Isar command for test p A particular feature of the local-variable management is the provision of definitions for ter and term‹pop› operations --- encoded as 🍋‹('o, 'σ) MONSE› operations --- which are vital f the function specifications defined below. ML‹ signature STATEMGT = sig structure Data: GENERIC_DATA datatype var_kind = global_var of typ | local_var of typ type state_field_tab = var_kind Symtab.table val MON_SE_T: typ -> typ -> typ val add_record_cmd: {overloaded: bool} -> bool -> (string * string option) list -> binding -> string option -> (binding * string * mixfix) list -> theory -> theory val add_record_cmd': {overloaded: bool} -> bool -> (string * string option) list -> binding -> string option -> (binding * typ * mixfix) list -> theory -> theory val add_record_cmd0: ('a -> Proof.context -> (binding * typ * mixfix) list * Proof.context) -> {overloaded: bool} -> bool -> (string * string option) list -> binding -> string option -> 'a -> theory -> theory val cmd: (binding * typ option * mixfix) option * (Attrib.binding * term) * term list * (binding * typ option * mixfix) list -> local_theory -> local_theory val construct_update: bool -> binding -> typ -> theory -> term val control_stateS: typ val control_stateT: typ val declare_state_variable_global: (typ -> var_kind) -> string -> theory -> theory val declare_state_variable_local: (typ -> var_kind) -> string -> Context.generic -> Context.ge val define_lense: binding -> typ -> binding * typ * 'a -> Proof.context -> local_theory val fetch_state_field: string * 'a -> (string * string) * 'a val filter_attr_of: string -> theory -> ((string * string) * var_kind) list val filter_name: string -> string * 'a -> ((string * string) * 'a) option val get_data: Proof.context -> Data.T val get_data_global: theory -> Data.T val get_result_value_conf: string -> theory -> (string * string) * var_kind val get_state_field_tab: Proof.context -> state_field_tab val get_state_field_tab_global: theory -> state_field_tab val get_state_type: Proof.context -> typ val get_state_type_global: theory -> typ val is_global_program_variable: Symtab.key -> theory -> bool val is_local_program_variable: Symtab.key -> theory -> bool val is_program_variable: Symtab.key -> theory -> bool val map_data: (Data.T -> Data.T) -> Context.generic -> Context.generic val map_data_global: (Data.T -> Data.T) -> theory -> theory val map_to_update: typ -> bool -> theory -> (string * string) * var_kind -> term -> term val merge_control_stateS: typ * typ -> typ val mk_global_state_name: binding -> binding val mk_lense_name: binding -> binding val mk_local_state_name: binding -> binding val mk_lookup_result_value_term: string -> typ -> theory -> term val mk_pop_def: binding -> typ -> typ -> Proof.context -> local_theory val mk_pop_name: binding -> binding val mk_push_def: binding -> typ -> Proof.context -> local_theory val mk_push_name: binding -> binding val new_state_record: bool -> (((string * string option) list * binding) * string option) option * (binding * string * mixfix) list -> theory -> theory val new_state_record': bool -> (((string * string option) list * binding) * typ option) option * (binding * typ * mixfix) list -> theory -> theory val new_state_record0: ({overloaded: bool} -> bool -> 'a list -> binding -> string option -> (binding * 'b * mixfix) list -> theory -> theory) -> bool -> (('a list * binding) * 'b option) option * (binding * 'b * mixfix) list -> theory -> theory val optionT: typ -> typ val parse_typ_'a: Proof.context -> binding -> typ val pop_eq: binding -> string -> typ -> typ -> Proof.context -> term val push_eq: binding -> string -> typ -> typ -> Proof.context -> term val read_fields: ('a * string * 'b) list -> Proof.context -> ('a * typ * 'b) list * Proof.context val read_parent: string option -> Proof.context -> (typ list * string) option * Proof.context val result_name: string val typ_2_string_raw: typ -> string val type_of: var_kind -> typ val upd_state_type: (typ -> typ) -> Context.generic -> Context.generic val upd_state_type_global: (typ -> typ) -> theory -> theory end structure StateMgt : 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("\<sigma>",sty)) end fun map_to_update sty is_pop thy ((struct_name, attr_name), local_var (Type("fun",[_,ty] let val tlT = if is_pop then Const(\<^const_name>\<open>List.tl\<close>, ty --> ty) else Const(\<^const_name>\<open>List.Cons\<close>, 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("\<sigma>",sty)) end 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("\<sigma>",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>\<open>unit\<close> 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 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("\<sigma>",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 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 lthy end fun add_record_cmd0 read_fields overloaded is_global_kind raw_params binding raw_parent 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 (aS, raw_fields) thy = let val state_index = (Int.toString o length o Symtab.dest) (StateMgt_core.get_state_field_tab_global thy) val state_pos = (Binding.pos_of o #1 o hd) raw_fields (*This hd is probably the reason why we can val ((raw_params, binding), res_ty) = case aS of SOME d => d | NONE => (([], Binding.make(state_index,state_pos)), NONE) 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'; fun clean_ctxt_parser b = Parse.$$$ "(" |-- (Parse.type_args_constrained -- Parse.binding) -- (if b then Scan.succeed NONE else Parse.typ >> SOME) --| Parse.$$$ ")" : (((string * string option) list * binding) * string option) parser val _ = Outer_Syntax.command 🍋‹global_vars› "define global state record" (Scan.option (clean_ctxt_parser true) -- Scan.repeat1 Parse.const_binding >> (Toplevel.theory o new_state_record true)); val _ = Outer_Syntax.command 🍋‹local_vars_test› "define local state record" (Scan.option (clean_ctxt_parser false) -- 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) 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 = let fun transform t1 t2 name ty = 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 in case tm of Const ("_type_constraint_", _) $ Const (@{const_name "Clean.syntax_assign"}, _) $ (t1 as Const ("_type_constraint_", _) $ Const (name, ty)) $ t2 => transform t1 t2 name ty | Const (@{const_name "Clean.syntax_assign"}, _) $ (t1 as Const ("_type_constraint_", _) $ Const (name, ty)) $ t2 => transform t1 t2 name ty | _ => abs tm end 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_position1 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 \<open> [(@{syntax_const "_cartouche_string"}, (fn ctxt => Clean_Syntax_Lift.string_tr ctxt (Symbol_Pos.cartouche_content o Symbol_Pos. \<close> section\<open>Support for (direct recursive) Clean Function Specifications \<close> text\<open>Based on the machinery for the State-Management and implicitly cooperating with th cartouches for assignment syntax, the function-specification \<^theory_text>\<open>functio \<^enum> the parsing and type-checking of parameters, \<^enum> the parsing and type-checking of pre and post conditions in MOAL notation (using \<open>\<lambda>\<close>-lifting cartouches and implicit reference to parameters, pre an \<^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>\<open>../examples/Quicksort_conc accompanying this distribution. \<close> text\<open>In order to support the \<^verbatim>\<open>old\<close>-notation known from JML and simi we introduce the following definition:\<close> definition old :: "'a \<Rightarrow> 'a" where "old x = x" text\<open>The core module of the parser and operation specification construct is implemented following module:\<close> ML \<open> 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 (🍋‹returns› |-- Parse.typ) "unit" val locals_clause = (Scan.optional ( 🍋‹local_vars› -- (Scan.repeat1 Parse.const_binding)) ("", [])) val parse_proc_spec = ( Parse.binding -- parse_param_decls -- parse_returns_clause --| 🍋‹pre› -- Parse.term --| 🍋‹post› -- Parse.term -- (Scan.option ( 🍋‹variant› |-- Parse.term)) -- (Scan.optional( 🍋‹local_vars› |-- (Scan.repeat1 Parse.const_binding))([])) --| 🍋‹defines› -- (Parse.position (Parse.term)) ) >> (fn ((((((((binding,params),ret_ty),pre_src),post_src),variant_src),locals)),bod { 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("σpre", sty, transform_old0 term) end fun define_cond binding f_sty transform_old check_absence_old cond_suffix params read_co 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 🍋) 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 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 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*Copyright 20182019 UniversitSaclay-, France val measure_term = case read_variant_opt of NONE => Free(bdg_ord_name,args_ty --> HOLogic.natT) * modification permitted the conditions val * --> 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.blockC"}, umty --> umty --> rmty --> rmty) $ Const(read_constname ctxt (Binding.name_of push_name),umty) $ (Const* APARTICULARDISCLAIMEDNO COPYRIGHT $ HOLogic.mk_tuple (map Free params')) $ Const(read_constname ctxt (Binding.name_of pop_name),rmty)) rhs_main_recwfrecT (Abs(bdg_rec_name, (args_ty --> rmty) , mk_pat_tupleabsparams (Const(@{const_name "Clean.blockC"}, umty-->umty->rmty $ Const $ (Constonstnamecore_name (args_ty $ (Bound $ HOLogic.mk_tuple (map Free params')) read_constnameof_e,y)java.lang.StringIndexOutOfBoundsException: Index 98 out of val eq_main = mk_meta_eq(lhs_main, if x then rhs_main_rec else rhs_main ) val args_main = (SOME(binding,NONE,NoSyndingtts,],] in ctxt |>"(<ga <Turnstile> ( _ ←)) σ M)" end val _ = Local_Theory.exit_result_global; val _ = Named_Target.theory_map_result; val _ = Named_Target exec_assign_globalD'=exec_assign_globallobalD1 (* This code is in large parts so messy because the extensible record package (used inside StateMgt.new_state_record) is onlyavailablestransformationnglobalcontextstexts which cuts the local context calculations into two halves. The second halves is cut again into two halves becausethe efinitionnitionf ore apparentlyoessnot keffect eforefiningnghelock structureen oteparated(his problemanperhaps vercome somehow)) Precondition: the terms of the read-functions e llypedinerespective local contexts. *) fun error "No measure required in non-recursive call" |checkNsem_function_spec_gen (isrec as {recursive :ool {bindinging_type,read_variant_opts, read_body, read_pre, read_post params} : funct_spec_sem thy = letfixesams_Tset_tytxt nctxt "\sigma<> ( _ \<eftarrowtarrow |> Proof_Cotex.ad_fixes (map (fnn s,ty)=>(s,SOME,NoS)) params_s) (* 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_resultassumes "exec_stopsigma (K (fn=ed_Targetmap (read_function_spec params, ret_type) #> addfixes ) y in thy' |> theory_map let valsty_old =StateMgt_core thy ( define_precond binding sty_old params #> define_postcondding_ty_oldd_post in parse_contract |> StateMgt.new_state_record false<>C_def |> theory_map ty t letly=teMgt_core xt pd params _ StateMgt_coreTet_tyy valle_k<equiv while_C" val ctxt' = if #recursive isrec then Proof_Context.add_fixes ,ME ags_ty--> mon_se_t,NSn)] ctxt |> #2 else ctxt =_ody ctx' os_t 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. *) |> theoapply(ssubst Monadwhhle__E_unfold) (fn params => fn ret_ty => fn cxt => let val sty = StateMgt_cget_st_yecx then show "\C b do" val body = read_body ctxt mon_se_ty in ctxt |> define_body_main isrec binding ret_ty sty params read_variant_opt body end)java.lang.StringIndexOutOfBoundsException: Index 30 out of bounds for length nd chec (isrec as {recu= _:bool}) ( {binding, ret_type, variant_src, loc"\sigma ⊨ ⊨C b then c ;- (while_k ;nset_break_stat body_src, pre_src, post_src, params} : funct_spec_src) thy = checkNsem_function_spec_genthod_setup@binding atch_tacbased matching { = 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 🍋‹function_spec› "define Clean function specification" (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = false})); val _ = Outer_Syntax.command 🍋‹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 :: "[('\<sigma>_ext) control_state_ext \<Rightarrow> bool, ('\<beta>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E, ('\<beta>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E] \<Rightarrow> ('\<beta>, ('\<sig where "if_C c E F = (\<lambda>\<sigma>. if exec_stop \<sigma> then Some(undefined, \<sigma>) \<comment> \<open>state unchanged, return arbitrary\<close> else if c \<sigma> then E \<sigma> else F \<sigma>)" syntax (xsymbols) "_if_SECLEAN" :: "['\<sigma> \<Rightarrow> bool,('o,'\<sigma>)MON\<^sub>S\<^sub>E,('o','\<sigma> (\<open>(if\<^sub>C _ then _ else _fi)\<close> [5,8,8]20) translations "(if\<^sub>C cond then T1 else T2 fi)" == "CONST Clean.if_C cond T1 T2" definition while_C :: "(('\<sigma>_ext) control_state_ext \<Rightarrow> bool) \<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E \<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "while_C c B \<equiv> (\<lambda>\<sigma>. if exec_stop \<sigma> then Some((), \<sigma>) else ((MonadSE.while_SE (\<lambda> \<sigma>. \<not>exec_stop \<sigma> \<and> c \<sigma>) B) ;- unset_break_status) \<sigma>)" syntax (xsymbols) "_while_C" :: "['\<sigma> \<Rightarrow> bool, (unit, '\<sigma>)MON\<^sub>S\<^sub>E] \<Rightarrow> (u (\<open>(while\<^sub>C _ do _ od)\<close> [8,8]20) translations "while\<^sub>C c do b od" == "CONST Clean.while_C c b" section\<open>Miscellaneous\<close> text\<open>Since \<^verbatim>\<open>int\<close> were mapped to Isabelle/HOL @{typ "int"} and \<^ve there is the need for a common interface for accesses in arrays, which were represented by Isabelle/HOL lists: \<close> consts nth\<^sub>C :: "'a list \<Rightarrow> 'b \<Rightarrow> 'a" overloading nth\<^sub>C \<equiv> "nth\<^sub>C :: 'a list \<Rightarrow> nat \<Rightarrow> 'a" begin definition nth\<^sub>C_nat : "nth\<^sub>C (S::'a list) (a) \<equiv> nth S a" end overloading nth\<^sub>C \<equiv> "nth\<^sub>C :: 'a list \<Rightarrow> int \<Rightarrow> 'a" begin definition nth\<^sub>C_int : "nth\<^sub>C (S::'a list) (a) \<equiv> nth S (nat a)" end definition while_C_A :: " (('\<sigma>_ext) control_state_scheme \<Rightarrow> bool) \<Rightarrow> (('\<sigma>_ext) control_state_scheme \<Rightarrow> nat) \<Rightarrow> (('\<sigma>_ext) control_state_ext \<Rightarrow> bool) \<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E \<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "while_C_A Inv f c B \<equiv> while_C c B" ML\<open> 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>\<open>bind_SE'\<close>, t --> t' --> t') $ C $ C' end; fun mk_seq_assign_C rhs lhs varname vartyp= let val t1 = fastype_of rhs val t2 = fastype_of lhs in Const(\<^const_name>\<open>bind_SE\<close>, t1 --> (vartyp --> t2) --> t2 ) $ rhs $ absfree (varname fun mk_skip_C sty = Const(\<^const_name>\<open>skip\<^sub>S\<^sub>E\<close>, StateMgt_core.MON_ fun mk_break sty = Const(\<^const_name>\<open>break\<close>, StateMgt_core.MON_SE_T HOLogic.unitT sty ) (* From dev-branch: don't know which version is better. bu 25.11.25 *) fun mk_return_C upd rhs = let val upd_ty = fastype_of upd val (rty, sty) = case upd_ty of Type("fun",[Type("fun", [Type(_(*list*),[r_ty]),_]), Type ("fun",[s_ty,_])]) => (r_ty, s_ty) | _=>error "mk_return_C: illegal type for update func" val rhs_ty = sty --> rty val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty in Const(🍋‹returnC›, upd_ty --> rhs_ty --> mty) $ upd $ rhs end (* overridden by afp version. *) 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(🍋‹returnC›, upd_ty --> rhs_ty --> mty) $ upd $ rhs end (* From dev-branch: don't know which version is better. bu 25.11.25 *) fun mk_assign_global_C upd rhs = let val upd_ty = fastype_of upd val (rty, sty) = case upd_ty of Type("fun",[Type("fun", [r_ty,_]), Type ("fun",[s_ty,_])]) => (r_ty, s_ty) | _=>error "mk_assign_global_C: illegal type for update func" val rhs_ty = sty --> rty val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty in Const(🍋‹assign_global›, upd_ty --> rhs_ty --> mty) $ upd $ rhs end (* overridden by afp version. *) 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(🍋‹assign_global›, upd_ty --> rhs_ty --> mty) $ upd $ rhs end (* From dev-branch: don't know which version is better. bu 25.11.25 *) fun mk_assign_local_C upd rhs = let val upd_ty = fastype_of upd val (rty, sty) = case upd_ty of Type("fun",[Type("fun", [Type(_(*list*),[r_ty]),_]), Type ("fun",[s_ty,_])]) => (r_ty, s_ty) | _=>error "mk_assign_local_C: illegal type for update func" val rhs_ty = sty --> rty val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty in Const(🍋‹assign_local›, upd_ty --> rhs_ty --> mty) $ upd $ rhs end (* overridden by afp version. *) 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(🍋‹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(🍋‹callC›, 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(🍋‹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(🍋‹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(🍋‹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(🍋‹blockC›, bty) $ push $ body $ pop end end;› section‹Function-calls in Expressions› text\<open>The precise semantics of function-calls appearing inside expressions is under-sp which is a notorious problem for compilers and analysis tools. In Clean, it is impossible by construction --- and the type discipline --- to have function-calls inside expressions. However, there is a somewhat \<^emph>\<open>recommended coding-scheme\<close> for this feature, issue to decisions in the front-end: @{verbatim [indent=10, indent=70] \<open>a = f() + g();\<close>} can be represented in Clean by: @{cartouche [indent=10, indent=70] \<open>x \<leftarrow> f(); y \<leftarrow> g(); \<open>a := x + y\<c @{cartouche [indent=10, indent=70] \<open>x \<leftarrow> g(); y \<leftarrow> f(); \<open>a := y + x\<c 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>\<open>f()\<close> and \<^verbatim>\<open>g() assumption is not necessarily justified in modern compilers, where actually neither of these two (atomic) serializations of \<^verbatim>\<open>f()\<close> and \<^verbatim>\<open>g()\<close> ma 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. \<close> end
¤ Dauer der Verarbeitung: 0.73 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09