Impressum Clean.thy

(******************************************************************************
 * 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
  C-like control-flow operators based on a shallow embedding into the ``State Exception Monads'' theory
  in 🍋‹MonadSE.thy›. It strives for a type-safe notation of program-variables, an
  construction of the typed state-space in order to facilitate incremental verification
  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 local variables.
 end{itemize}

  that Clean in its current version is restricted to 🪙‹monomorphic› global and local variables
  well as function parameters. This limitation will be overcome at a later stage. The construction
  itself, however, is deeply based on parametric polymorphism (enabling structured proofs over
  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, 'σ) MON_SE = ‹'σ ⇀ ('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› constructed by a
  of extensible record definitions:
 🪙 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}
 🪙‹control_state› represents the $\sigma_0$ state.
 🪙 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}
 🪙 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 🍋‹_ list›-lifting is used to model a 🪙‹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 🪙‹record› package creates an 🪙‹'σ› extensible record type
 🪙‹'σ control_state_ext› where the 🪙‹'σ› stands for extensions that are subsequently ``stuffed'' in
 . Furthermore, it generates definitions for the constructor, accessor and update functions and
  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
  of these theorems constitutes the 🪙‹memory model› of Clean, providing an incrementally
  state-space for global and local program variables. In contrast to axiomatizations
  memory models, our generated state-spaces might be ``wrong'' in the sense that they do not
  the operational behaviour of a particular compiler or a sufficiently large portion of the
  language; however, it is by construction 🪙‹logically consistent› since it is
  to derive falsity from the entire set of conservative extension schemes used in their
 . A particular advantage of the incremental state-space construction is that it
  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
  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_SE"
  where   "break ≡ (λ σ. Some((), σ ( break_status := True )))"
  
definition unset_break_status :: "(unit, ('σ_ext) control_state_ext) MON_SE"
  where   "unset_break_status ≡ (λ σ. Some((), σ ( break_status := False )))"

definition set_return_status :: " (unit, ('σ_ext) control_state_ext) MON_SE"    
  where   "set_return_status = (λ σ. Some((), σ ( return_status := True )))"
    
definition unset_return_status :: "(unit, ('σ_ext) control_state_ext) MON_SE"    
  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_L 
  where "break_status_L = create_L control_state.break_status control_state.break_status_update"
lemma "vwb_lens break_status_L"
  unfolding break_status_{L_def}
  by (simp add: vwb_lens_def  create_{L_def} wb_lens_def mwb_lens_def 
                mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def)



definition return_status_L 
  where "return_status_L = create_L control_state.return_status control_state.return_status_update"
lemma "vwb_lens return_status_L"
  unfolding return_status_{L_def}
  by (simp add: vwb_lens_def  create_{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_L ⋈ return_status_L "
  by (simp add: break_status_{L_def} lens_indepI return_status_{L_def} upd2put_def create_{L_def})

definition strong_control_independence  (‹♯!›)
  where "♯! L = (break_status_L ⋈ L ∧ return_status_L ⋈ L)"

lemma "vwb_lens break_status_L"
  unfolding vwb_lens_def break_status_{L_def} create_{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_{L_def} lens_indep_def return_status_{L_def} upd2put_def create_{L_def})

lemma expimnt :"♯! (create_L getv updv) ==> (λf σ. updv (λ_. f (getv σ)) σ) = updv"
  unfolding create_{L_def} strong_control_independence_def 
            break_status_{L_def} return_status_{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_L getv updv) ==> (λf σ. updv (λ_. f (getv σ)) σ) = updv"
  unfolding create_{L_def} strong_control_independence_def lens_indep_def
            break_status_{L_def} return_status_{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_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_{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_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_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
  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› with some local
  ‹tmp› is defined:
 🪙‹record state2 = state1 + tmp :: "nat stack" result_value :: "nat stack" ›, where the ‹stack›
  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
  of the assignment. The trick to do this in a generic 🪙‹and› type-safe way is to provide
  generated accessor and update functions (the ``lens'' representing this global variable,
 . cite‹"Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and
 DBLP:conf/ictac/FosterZW16"›) to the generic assign operators. This pair of accessor and update
  all relevant semantic and type information of this particular variable and 🪙‹characterizes›
  variable semantically. Specific syntactic support~🪙‹via the Isabelle concept of
 : 🪙‹https://isabelle.in.tum.de/doc/isar-ref.pdf›› will hide away the syntactic overhead
  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_SE"
  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_SE" (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 done
  @{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 a stack
  order to support individual instances in case of function recursion. This requires
  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) MON_SE"  (infix ‹:==_L› 100)
  where    "assign_local upd rhs = assign(λσ. ((upd o upd_hd) (%_. rhs σ)) σ)"


text‹Semantically, the difference between 🪙‹global› and 🪙‹local› is rather unimpressive as the
 following lemma shows. However, the distinction matters for the pretty-printing setup of Clean.›
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 assignment to a local
  ‹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
  this case.›

definition return_C0
  where   "return_C0 A = (λσ. if exec_stop σ then Some((), σ)
                                            else (A ;- set_return_status) σ)"

definition return_C :: "(('a list ==> 'a list) ==> 'σ_ext control_state_scheme ==> 'σ_ext control_state_scheme)
                      ==> ('σ_ext control_state_scheme ==> 'a)
                      ==> (unit,'σ_ext control_state_scheme) MON_SE" (‹return🍋›)
  where   "return_C upd rhs = return_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‹
  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
  operation generated by the 🪙‹record›-package, which is generated while treating local variables
  ‹swap›. By the way, a stack for ‹return›-values is also generated in order to give semantics
  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› operations,
  which suitable definitions are generated as well:

 {cartouche [display]
 ‹definition push_local_swap_state :: "(unit,'a local_swap_state_scheme) MON_SE"
 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_SE"
 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 concrete
  ‹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
  the previous section; the declarations of global and local variable blocks are constructed by
  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 Clean state"

  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) 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\<open> On the managed local state-spaces, it is now straight-forward to define the semantics for 
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 follows:

@{cartouche [display]
\<open>definition swap_core :: "nat \<times> nat \<Rightarrow>  (unit,'a local_swap_state_scheme) MON\<^sub>S\<^sub>E"
    where "swap_core  \<equiv> (\<lambda>(i,j). ((assign_local tmp_update (\<lambda>\<sigma>. A \<sigma> ! i ))   ;-
                            (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>S\<^sub>E"
  where   "swap \<equiv> \<lambda>(i,j). block\<^sub>C push_local_swap_state (swap_core (i,j)) pop_local_swap_state"
\<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>return\<^bsub>upd\<^esub>\<close>-aware.\<close>

definition call\<^sub>C :: "( '\<alpha> \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E) \<Rightarrow>
                       ((('\<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, \<sigma>) else M (A\<^sub>1 \<sigma>) \<sigma>)"

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 arguments.
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 \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E"
  where   "call_0\<^sub>C M = (\<lambda>\<sigma>. if exec_stop \<sigma> then Some(undefined, \<sigma>) else M \<sigma>)"

text\<open>The generic version using tuples is identical with @{term \<open>call_1\<^sub>C\<close>}.\<close>
definition call_1\<^sub>C :: "( '\<alpha> \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E) \<Rightarrow>
                       ((('\<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) control_state_ext)MON\<^sub>S\<^sub>E) \<Rightarrow>
                       ((('\<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(undefined, \<sigma>) else M (A\<^sub>1 \<sigma>) (A\<^sub>2 \<sigma>) \<sigma>)"

definition call_3\<^sub>C :: "( '\<alpha> \<Rightarrow> '\<beta> \<Rightarrow>  '\<gamma> \<Rightarrow> ('\<rho>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E) \<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 Some(undefined, \<sigma>) 
                                                   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 style of
 {ML_structure "HOLogic"} from the Isabelle/HOL libraries. They incorporate the construction
  types during term construction in a bottom-up manner. Consequently, the leafs of such
  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 t))
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 provides the 
functionality for the commands keywords 🪙‹global_vars›, 🪙‹local_vars›  and 🪙‹local_vars_test›.
Note that the difference between 🪙‹local_vars› and 🪙‹local_vars_test› is just a technical one:
🪙‹local_vars› can only be used inside a Clean function specification, made with the 🪙‹function_spec›
command. On the other hand, 🪙‹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 🍋‹('o, 'σ) MON_SE› operations --- which are vital for
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.generic
    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]))) term = 
       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 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 (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 cant have empty local vars*)
        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.explode)))]
\<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 the 
cartouches for assignment syntax, the function-specification \<^theory_text>\<open>function_spec\<close>-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 \<open>\<lambda>\<close>-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>\<open>../examples/Quicksort_concept.thy\<close>-example,
accompanying this distribution.
\<close>


text\<open>In order to support the \<^verbatim>\<open>old\<close>-notation known from JML and similar annotation languages,
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 in the
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)),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("σ_pre", 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 🍋)
           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.block_C"}, 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.block_C"}, 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 bounds for length 98
           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 30
       nd

    chec (isrec as {recu= _:bool})
                               ( {binding, ret_type, variant_src, loc"\sigma ⊨ ⊨C b then c ;- (while_k ;nset_break_statustatuskipsubSjava.lang.NullPointerException
                                  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>, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E"
  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>)MON\<^sub>S\<^sub>E] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>E" 
          (\<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> (unit, '\<sigma>)MON\<^sub>S\<^sub>E" 
          (\<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 \<^verbatim>\<open>unsigned int\<close> to @{typ "nat"},
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, vartyp) lhs end;

fun mk_skip_C sty = Const(\<^const_name>\<open>skip\<^sub>S\<^sub>E\<close>, StateMgt_core.MON_SE_T HOLogic.unitT sty)

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(🍋‹return_C›, 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(🍋‹return_C›, 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(🍋‹call_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(🍋‹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(🍋‹block_C›, bty) $ push $ body $ pop end  

end;›

section‹Function-calls in Expressions›

text\<open>The precise semantics of function-calls appearing inside expressions is under-specified in C,
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, which leaves this
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\<close> \<close>} or 
@{cartouche [indent=10, indent=70] \<open>x \<leftarrow> g(); y \<leftarrow> f(); \<open>a := y + x\<close> \<close>}

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()\<close> are atomic actions; note that this 
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> 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.  
\<close>

end