SSL hoare_syntax.ML

(*  Title:      hoare_syntax.ML
    Author:     Norbert Schirmer, TU Muenchen

Copyright (C) 2004-2007 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.
*)

(* fixme: Adapt guard generation to new syntax of op + etc. *)

signature HOARE_SYNTAX =
sig
  val antiquoteCur: string
  val antiquoteOld: string
  val antiquoteOld_tr: Proof.context -> term list -> term
  val antiquote_applied_only_to: (term -> bool) -> term -> bool
  val antiquote_varname_tr: string -> term list -> term
  val app_quote_tr': Proof.context -> term -> term list -> term
  val assert_tr': Proof.context -> term list -> term
  val assign_tr': Proof.context -> term list -> term
  val assign_tr: Proof.context -> term list -> term
  val basic_assigns_tr: Proof.context -> term list -> term
  val basic_tr': Proof.context -> term list -> term
  val basic_tr: Proof.context -> term list -> term
  val bexp_tr': string -> Proof.context -> term list -> term
  val bind_tr': Proof.context -> term list -> term
  val call_ass_tr: bool -> bool -> term list -> Proof.context -> term list -> term
  val call_tr': Proof.context -> term list -> term
  val call_exn_tr': Proof.context -> term list -> term
  val call_tr: bool -> bool -> term list -> Proof.context -> term list -> term
  val dyn_call_tr': Proof.context -> term list -> term
  val dyn_call_exn_tr': Proof.context -> term list -> term
  val fcall_tr': Proof.context -> term list -> term
  val fcall_tr: Proof.context -> term list -> term
  val guarded_Assign_tr: Proof.context -> term list -> term
  val guarded_Cond_tr: Proof.context -> term list -> term
  val guarded_NNew_tr: Proof.context -> term list -> term
  val guarded_New_tr: Proof.context -> term list -> term
  val guarded_WhileFix_tr: Proof.context -> term list -> term
  val guarded_While_tr: Proof.context -> term list -> term
  val guards_tr': Proof.context -> term list -> term
  val hide_guards: bool Config.T
  val init_tr': Proof.context -> term list -> term
  val init_tr: Proof.context -> term list -> term
  val loc_tr': Proof.context -> term list -> term
  val loc_tr: Proof.context -> term list -> term
  val new_tr : Proof.context -> term list -> term
  val new_tr': Proof.context -> term list -> term
  val nnew_tr : Proof.context -> term list -> term
  val nnew_tr': Proof.context -> term list -> term
  val proc_ass_tr: Proof.context -> term list -> term
  val proc_tr': Proof.context -> term list -> term
  val proc_tr: Proof.context -> term list -> term
  val quote_mult_tr': Proof.context -> (term -> bool) -> string -> string -> term -> term
  val quote_tr': Proof.context -> string -> term -> term
  val quote_tr: Proof.context -> string -> term -> term
  val raise_tr': Proof.context -> term list -> term
  val raise_tr: Proof.context -> term list -> term
  val switch_tr': Proof.context -> term list -> term
  val update_comp: Proof.context -> Hoare.lense option -> string list -> bool -> bool -> xstring -> term -> term -> term
  val use_call_tr': bool Config.T
  val whileAnnoGFix_tr': Proof.context -> term list -> term
  val whileAnnoG_tr': Proof.context -> term list -> term
end;

structure Hoare_Syntax: HOARE_SYNTAX =
struct

val use_call_tr' = Attrib.setup_config_bool @{binding hoare_use_call_tr'} (K true);
val hide_guards = Attrib.setup_config_bool @{binding hoare_hide_guards} (K false);

val globalsN = "globals";
val localsN = "locals";
val globals_updateN = suffix Record.updateN globalsN;
val locals_updateN = suffix Record.updateN localsN;
val upd_globalsN = "upd_globals";   (* fixme authentic syntax !? *)
val allocN = "alloc_'";
val freeN = "free_'";

val Null = Syntax.free "Simpl_Heap.Null";   (* fixme ?? *)


(** utils **)

(* transpose [[a,b],[c,d],[e,f]] = [[a,c,d],[b,d,f]] *)
fun transpose [[]] = [[]]
  | transpose ([]::xs) = []
  | transpose ((y::ys)::xs) = (y::map hd xs)::transpose (ys::map tl xs)

fun maxprefix eq ([], ys) = []
  | maxprefix eq (xs, []) = []
  | maxprefix eq ((x::xs),(y::ys)) = if eq (x,y)
                                     then x::maxprefix eq (xs,ys)
                                     else []

fun maxprefixs eq [] = []
  | maxprefixs eq [[]] = []
  | maxprefixs eq xss = foldr1 (maxprefix eq) xss;

fun mk_list [] = Syntax.const @{const_syntax Nil}
  | mk_list (x::xs) = Syntax.const @{const_syntax Cons} $ x $ mk_list xs;

(* convert Fail to Match, useful for print translations *)
fun unsuffix' sfx a = unsuffix sfx a handle Fail _ => raise Match;
fun unsuffixI sfx a = unsuffix sfx a handle Fail _ => a;

fun is_prefix_or_suffix s t =
  can (unprefix s) t orelse can (unsuffix s) t;


fun is_other ctxt = case Hoare.get_default_state_kind ctxt of Hoare.Other _ => true | _ => false

(** hoare data **)

fun is_global_comp ctxt name =
  let
    val res = case Hoare.get_default_state_space ctxt of
                SOME {is_defined, ...} => not (is_defined ctxt name)
              | _ =>
                (case StateSpace.get_comp' (Context.Proof ctxt) name of
                  SOME (_, lns) => forall (fn ln => is_prefix_or_suffix "globals" (Long_Name.base_name ln)) lns
                | NONE => false)
  in
    res
  end

(** parsing and printing **)

(* quote/antiquote *)

val antiquoteCur = @{syntax_const "_antiquoteCur"};
val antiquoteOld = @{syntax_const "_antiquoteOld"};

fun intern_const_syntax consts =
  Consts.intern_syntax consts #> perhaps Long_Name.dest_hidden;

fun is_global ctxt name =
  let
    val thy = Proof_Context.theory_of ctxt;
    val consts = Proof_Context.consts_of ctxt;
  in
    (case Sign.const_type thy (intern_const_syntax consts name) of
      NONE => is_global_comp ctxt name
    | SOME T => String.isPrefix globalsN (Long_Name.base_name (fst (dest_Type (domain_type T)))))
    handle Match => false
  end;

exception UNDEFINED of string

(* fixme: if is_state_var etc. is reimplemented, rethink about when adding the deco to
   the records *)

fun first_successful_tr _ [] = raise TERM ("first_successful_tr: no success",[])
  | first_successful_tr f [x] = f x
  | first_successful_tr f (x::xs) = f x handle TERM _ => first_successful_tr f xs;

fun statespace_lookup_tr ctxt ps s n =
  case Hoare.get_default_state_space ctxt of
    SOME {lookup_tr, ...} => lookup_tr ctxt n $ s
  | _ =>
      let
        val cn = map Hoare.clique_name (#active_procs (Hoare.get_data ctxt));
        val procs = ps @ cn;
        val names =
          (Hoare.name_tr ctxt true n) :: map (fn p => (suffix (Hoare.par_deco p) (unsuffixI Hoare.deco n))) procs;
      in
        first_successful_tr (StateSpace.gen_lookup_tr ctxt s) names
      end

fun K_rec_syntax v = Abs ("_", dummyT, incr_boundvars 1 v);

fun statespace_update_tr ctxt NONE ps id n v =
      (case Hoare.get_default_state_space ctxt of
        SOME {update_tr, ...} => update_tr ctxt n $ K_rec_syntax v
      | _ =>
        let
          fun gen_update_tr id ctxt n v =
            StateSpace.gen'_update_tr true id ctxt n v (Bound 0) |> dest_comb |> fst

          val cn = map Hoare.clique_name (#active_procs (Hoare.get_data ctxt));
          val procs = ps @ cn;
          val names =
            (Hoare.name_tr ctxt true n) :: map (fn p => (suffix (Hoare.par_deco p) (unsuffixI Hoare.deco n))) procs;
        in first_successful_tr (fn n => gen_update_tr id ctxt n v) names
        end)
  | statespace_update_tr ctxt (SOME {lookup, update}) ps id n v =
      update $ K_rec_syntax v


local
  fun is_record_sel ctxt nm =
    let
      val SOME (Const (c, T)) = try (Syntax.read_term ctxt) nm
      val recT = domain_type T
      val (flds, _) = Record.get_recT_fields (Proof_Context.theory_of ctxt) recT
    in member (op =) (map fst flds) c end
    handle TYPE _ => false
         | Bind  => false
         | Match => false
in

fun lookup_comp ctxt ps name =
  if is_record_sel ctxt name
  then
    if is_global ctxt name
    then (fn s => Syntax.free name $ (Syntax.free "globals" $ s))
    else (fn s => Syntax.free name $ s)
  else
    let
      val sel = Syntax.const (if is_global_comp ctxt name then "globals" else "locals");
    in (fn s => statespace_lookup_tr ctxt ps (sel $ s) name) end;

(*
fixme:
update of global and local components:
One should generally provide functions:
glob_upd:: ('g => 'g) => 's => 's
loc_upd:: ('l => 'l) => 's => 's
so that global and local updates can nicely be composed.
loc_upd for the record implementation is vacuous.
Right now for example an assignment of NEW to a global variable returns
a funny repeated update of global components...

This would make the composition more straightforward...
Basically one wants the map on a component rather then the update. Maps can
be composed nicer...
*)


fun update_comp ctxt lense_opt ps atomic id name value =
  if is_record_sel ctxt name
  then
    let
      val upd = Syntax.free (suffix Record.updateN name) $ K_rec_syntax value;
    in
      if atomic andalso is_global ctxt name
      then (fn s =>
        Syntax.free globals_updateN $ (*(K_rec_syntax*) upd  $ s)
      else (fn s => upd $ s)
    end
  else
    let
      val reg = if is_global_comp ctxt name then "globals" else "locals";
      val upd = Syntax.free (reg ^ Record.updateN);
      val sel = Syntax.free reg;
    in
      fn s =>
        if atomic then
          upd $ statespace_update_tr ctxt lense_opt ps id name value $ s
        else statespace_update_tr ctxt lense_opt ps id name value $ s
    end;

end;

fun antiquote_global_tr ctxt off i t =
  let
    fun mk n t = lookup_comp ctxt [] n (Bound (i + off n));
     (*if is_global ctxt n then t$(Free ("globals",dummyT)$Bound (i + off n))
       else t$Bound (i + off n)*)
  in
    (case t of
      Free  (n, _) => mk n t
    | Const (n, _) => mk n t
    | _ => t $ Bound i)
  end;


fun antiquote_off_tr offset ctxt name =
  let
    fun tr i ((t as Const (c, _)) $ u) =
          if c = name then antiquote_global_tr ctxt offset i (tr i u)
          else tr i t $ tr i u
      | tr i (t $ u) = tr i t $ tr i u
      | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
      | tr _ a = a;
  in tr 0 end;


val antiquote_tr = antiquote_off_tr (K 0)

fun quote_tr ctxt name t = Abs ("s", dummyT, antiquote_tr ctxt name (Term.incr_boundvars 1 t));

fun antiquoteCur_tr ctxt t = antiquote_tr ctxt antiquoteCur (Term.incr_boundvars 1 t);


fun antiquote_varname_tr anti [n] =
  (case n of
    Free (v, T) => Syntax.const anti $ Free (Hoare.varname v, T)
  | Const (c, T) => Syntax.const anti $ Const (Hoare.varname c, T)
  | _ => Syntax.const anti $ n);



fun antiquoteOld_tr ctxt [s, n] =
  (case n of
    Free (v, T) => lookup_comp ctxt [] (Hoare.varname v) s
  | Const (c, T) => lookup_comp ctxt [] (Hoare.varname c) s
  | _ => n $ s);

fun first_match [] t = raise Match
  | first_match (f::fs) t = f t handle Match => first_match fs t

fun lookup_tr' ctxt t = t |> first_match [
  fn t =>
    case Hoare.get_default_state_space ctxt of
     SOME {lookup_tr', ...} => lookup_tr' ctxt t
   | NONE => raise Match,
  fn t => Hoare.undeco ctxt t]


fun antiquote_tr' ctxt name =
  let
    fun is_state i t =
      (case t of
        Bound j => i = j
      | Const (g,_) $ Bound j =>
          i = j andalso member (op =) [globalsN, localsN] (Long_Name.base_name g)
      | _ => false);
    fun tr' i (t $ u) =
       if is_state i u then Syntax.const name $ tr' i (lookup_tr' ctxt t)
       else tr' i t $ tr' i u
      | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
      | tr' i a = if a = Bound i then raise Match else a;
  in tr' 0 end;

fun quote_tr' ctxt name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' ctxt name t)
  | quote_tr' ctxt name (t as (Const _)) (* eta contracted *) =
      Syntax.const name $ Hoare.undeco ctxt t
  | quote_tr' _ _ _ = raise Match;



local
fun state_test (t as Const (g,_) $ u) f  =
      if member (op =) [localsN, globalsN] (Long_Name.base_name g) then f u else f t
  | state_test u f = f u;
in

fun antiquote_applied_only_to P =
  let
     fun test i (t $ u) =
       state_test u
         (fn Bound j =>
               if j=i then  P t
               else test i t andalso test i u
           | u => test i t andalso test i u)
       | test i (Abs (x, T, t)) = test (i + 1) t
       | test i _ = true;
  in test 0 end;



fun antiquote_mult_tr' ctxt is_selector current old  =
  let
    fun tr' i (t $ u) =
          state_test u
            (fn Bound j =>
                  if j = i then Syntax.const current $ tr' i (lookup_tr' ctxt t)
                  else if is_selector t (* other quantified states *)
                  then Syntax.const old $ Bound j $ tr' i (lookup_tr' ctxt t)
                  else  tr' i t $ tr' i u
              | pre as ((Const (m,_) $ Free _)) (* pre state *) =>
                  if (m = @{syntax_const "_bound"} orelse m = @{syntax_const "_free"})
                    andalso is_selector t
                  then Syntax.const old $ pre $ tr' i (lookup_tr' ctxt t)
                  else tr' i t $ pre
              | pre as ((Const (m,_) $ Var _)) (* pre state *) =>
                  if m = @{syntax_const "_var"} andalso is_selector t
                  then Syntax.const old $ pre $ tr' i (lookup_tr' ctxt t)
                  else tr' i t $ pre
              | u => tr' i t $ tr' i u)
      | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
      | tr' i a = if a = Bound i then raise Match else a;
  in tr' 0 end;
end;

fun quote_mult_tr' ctxt is_selector current old  (Abs (_, _, t)) =
      Term.incr_boundvars ~1 (antiquote_mult_tr' ctxt is_selector current old t)
  | quote_mult_tr' _ _ _ _ _ = raise Match;

fun app_quote_tr' ctxt f (t :: ts) =
      Term.list_comb (f $ quote_tr' ctxt antiquoteCur t, ts)
  | app_quote_tr' _ _ _ = raise Match;

fun app_quote_mult_tr' ctxt is_selector f (t :: ts) =
      Term.list_comb (f $ quote_mult_tr' ctxt is_selector antiquoteCur antiquoteOld  t, ts)
  | app_quote_mult_tr' _ _ _ _ = raise Match;



fun atomic_var_tr ctxt ps name value =
  update_comp ctxt NONE ps true false name value;


fun heap_var_tr ctxt hp p value =
  let
    fun upd s =
      update_comp ctxt NONE [] true false hp
        (Syntax.const @{const_syntax fun_upd} $ lookup_comp ctxt [] hp s $ p $ value) s;
  in upd end;

fun get_arr_var (Const (@{const_syntax List.nth},_) $ arr $ i) =
      (case get_arr_var arr of
         SOME (name,p,is) => SOME (name,p,i::is)
       | NONE => NONE)
  | get_arr_var (Const (@{syntax_const "_antiquoteCur"},_) $ Free (var,_)) =
     if Hoare.is_state_var var then SOME (var,NONE,[]) else NONE
  | get_arr_var (Const (@{syntax_const "_antiquoteCur"},_) $ Const (var,_)) =
     if Hoare.is_state_var var then SOME (var,NONE,[]) else NONE
  | get_arr_var ((Const (@{syntax_const "_antiquoteCur"},_) $ Free (hp,_)) $ p) =
     if Hoare.is_state_var hp then SOME (hp,SOME p,[]) else NONE
  | get_arr_var ((Const (@{syntax_const "_antiquoteCur"},_) $ Const (hp,_)) $ p) =
     if Hoare.is_state_var hp then SOME (hp,SOME p,[]) else NONE
  | get_arr_var _ = NONE


fun arr_var_tr ctxt ps name arr pos value idxs  =
  let
    fun sel_tr [] = arr
      | sel_tr (i::is) = Syntax.const @{const_syntax nth} $ sel_tr is $ i;

    fun lupd_tr value [] _ = value
      | lupd_tr value (i::is) idxs  =
          Syntax.const @{const_syntax list_update} $ sel_tr idxs $ i $ lupd_tr value is (i::idxs);


    val value' = lupd_tr value idxs [];
  in case pos of
       NONE   => atomic_var_tr ctxt ps name value'
     | SOME p => heap_var_tr ctxt name p value'
  end;

fun get_arr_mult_var (Const (@{syntax_const "_antiquoteCur"},_) $ Free (var,_)) =
     if Hoare.is_state_var var then SOME (var,NONE) else NONE
  | get_arr_mult_var (Const (@{syntax_const "_antiquoteCur"},_) $ Const (var,_)) =
     if Hoare.is_state_var var then SOME (var,NONE) else NONE
  | get_arr_mult_var ((Const (@{syntax_const "_antiquoteCur"},_) $ Free (hp,_)) $ p) =
     if Hoare.is_state_var hp then SOME (hp,SOME p) else NONE
  | get_arr_mult_var ((Const (@{syntax_const "_antiquoteCur"},_) $ Const (hp,_)) $ p) =
     if Hoare.is_state_var hp then SOME (hp,SOME p) else NONE
  | get_arr_mult_var _ = NONE

fun arr_mult_var_tr ctxt ps name arr pos vals idxs  =
  let
    val value' = Syntax.const @{const_syntax list_multupd} $ arr $ idxs $ vals;
  in
    case pos of
      NONE => atomic_var_tr ctxt ps name value'
    | SOME p => heap_var_tr ctxt name p value'
  end;

fun update_tr ctxt ps off_var off_val e arg =
  (case Term_Position.strip_positions arg of
    v as Const (@{syntax_const "_antiquoteCur"},_) $ Free (var,_) =>
      if Hoare.is_state_var var then atomic_var_tr ctxt ps var e
      else raise TERM ("no proper lvalue", [v])
  | (v as Const (@{syntax_const "_antiquoteCur"},_) $ Free (hp, _)) $ p =>
      if Hoare.is_state_var hp
      then heap_var_tr ctxt hp (antiquote_off_tr off_val ctxt antiquoteCur p) e
      else raise TERM ("no proper lvalue", [v])
  | v as Const (@{const_syntax list_multsel}, _) $ arr $ idxs =>
      (case get_arr_mult_var arr of
         SOME (var, pos) =>
            let
              val pos' = Option.map (antiquote_off_tr off_val ctxt antiquoteCur) pos;
              val var' = lookup_comp ctxt ps var (Bound (off_var var));
              val arr' = case pos' of NONE => var' | SOME p => var' $ p;
              val idxs' = antiquote_off_tr off_val ctxt antiquoteCur idxs;
            in arr_mult_var_tr ctxt ps var arr' pos' e idxs' end
       | NONE =>  raise TERM ("no proper lvalue", [v]))
  | v =>
      (case get_arr_var v of
        SOME (var,pos,idxs) =>
          let
            val pos' = Option.map (antiquote_off_tr off_val ctxt antiquoteCur) pos;
            val var' = lookup_comp ctxt ps var (Bound (off_var var));
            val arr' = case pos' of NONE => var' | SOME p => var' $ p;
            val idxs' = rev (map (antiquote_off_tr off_val ctxt antiquoteCur) idxs);
          in arr_var_tr ctxt ps var arr' pos' e idxs' end
      | NONE => raise TERM ("no proper lvalue", [v])))


fun app_assign_tr f ctxt [v, e] =
      let
        fun offset _ = 0;
      in f $ Abs ("s", dummyT, update_tr ctxt [] offset offset (antiquoteCur_tr ctxt e) v (Bound 0))
      end
  | app_assign_tr _ _ ts = raise TERM ("assign_tr", ts);


val assign_tr = app_assign_tr (Syntax.const @{const_syntax Basic});
val raise_tr = app_assign_tr (Syntax.const @{const_syntax raise});


fun basic_assign_tr ctxt (ts as [v, e]) =
      let
        fun offset v = 0;
      in update_tr ctxt [] offset offset (antiquoteCur_tr ctxt e) v
      end
  | basic_assign_tr _ ts = raise TERM ("basic_assign_tr", ts);

fun basic_assigns_tr ctxt [t] =
      let
        fun dest_basic (Const (@{syntax_const "_BAssign"}, _) $ v $ e) =
              basic_assign_tr ctxt [v,e]
          | dest_basic _ = raise Match;

        fun dest_basics (Const (@{syntax_const "_basics"}, _) $ x $ xs) =
              dest_basic x :: dest_basics xs
          | dest_basics (t as Const (@{syntax_const "_BAssign"}, _) $_ $ _) =
              [dest_basic t]
          | dest_basics _ = []
        val upds = dest_basics t;
      in Abs ("s", dummyT, fold (fn upd => fn s => upd s) upds (Bound 0))
      end
  | basic_assigns_tr _ ts = raise TERM ("basic_assigns_tr", ts);

fun basic_tr ctxt [t] =
  Syntax.const @{const_syntax Basic} $
    (Abs ("s", dummyT,
      antiquote_tr ctxt @{syntax_const "_antiquoteCur"} (Term.incr_boundvars 1 t) $ Bound 0));

fun init_tr ctxt args =
  (case map Term_Position.strip_positions args of
    [Const (var,_),comp,value] =>
      let
        fun dest_set (Const (@{const_syntax Set.empty}, _)) = []
          | dest_set (Const (@{const_syntax insert}, _) $ x $ xs) = x :: dest_set xs;

        fun dest_list (Const (@{const_syntax Nil}, _)) = []
          | dest_list (Const (@{const_syntax Cons}, _) $ Free (x, _) $ xs) = x :: dest_list xs;

        fun dest_val_list (Const (@{const_syntax Nil}, _)) = []
          | dest_val_list (Const (@{const_syntax Cons},_) $ x $ xs) =
              dest_set x :: dest_val_list xs
          | dest_val_list t = [dest_set t];

        val values =
          (case value of
            Const (@{const_syntax Cons}, _) $ _ $ _ =>
              map mk_list (transpose (dest_val_list value))
          | Const (@{const_syntax insert}, _) $ _ $ _ =>
              dest_set value
          | _ => raise TERM ("unknown variable initialization", []))
        val comps = dest_list comp;
        fun mk_upd var c v =
          Syntax.free (suffix Record.updateN (Hoare.varname (suffix ("_" ^ c) var))) $ v;
        val upds = map2 (mk_upd var) comps values;
        val app_upds = fold (fn upd => fn s => upd $ s) upds;
        val upd =
          if is_global ctxt (Hoare.varname (suffix ("_" ^ hd comps) var)) then
            Syntax.free (suffix Record.updateN globalsN) $
              app_upds (Syntax.free globalsN $ Bound 0) $ Bound 0
          else app_upds (Bound 0)
      in
        Syntax.const @{const_syntax Basic} $ Abs ("s", dummyT, upd)
      end
  | _ => raise Match);


fun new_tr ctxt (ts as [var,size,init]) =
      let
        fun offset v = 0;
        fun dest_init (Const (@{syntax_const "_newinit"}, _) $ Const (var, _) $ v) = (var, v)
          | dest_init _ = raise Match;

        fun dest_inits (Const (@{syntax_const "_newinits"}, _) $ x $ xs) =
              dest_init x :: dest_inits xs
          | dest_inits (t as (Const (@{syntax_const "_newinit"}, _) $_ $ _)) = [dest_init t]
          | dest_inits _ = raise Match;

        val g = Syntax.free globalsN $ Bound 0;
        val alloc = lookup_comp ctxt [] allocN (Bound 0);
        val new = Syntax.free "new" $ (Syntax.const @{const_syntax set} $ alloc);  (* fixme new !? *)

        fun mk_upd (var,v) =
          let
            val varn = Hoare.varname var;
            val var' = lookup_comp ctxt [] varn (Bound 0);
          in
            update_comp ctxt NONE [] false false varn
              (Syntax.const @{const_syntax fun_upd} $ var' $ new $ v)
          end;

        val inits = map mk_upd (dest_inits init);
        val free = lookup_comp ctxt [] freeN (Bound 0);
        val freetest = Syntax.const @{const_syntax Orderings.less_eq} $ size $ free;

        val alloc_upd =
          update_comp ctxt NONE [] false false allocN
            (Syntax.const @{const_syntax Cons} $ new $ alloc);
        val free_upd =
          update_comp ctxt NONE [] false false freeN
            (Syntax.const @{const_syntax Groups.minus} $ free $ size);

        val g' =
          Syntax.free (suffix Record.updateN globalsN) $
            K_rec_syntax (fold (fn upd => fn s => upd s) (alloc_upd :: free_upd :: inits) g) $
            Bound 0;
        val cond =
          Syntax.const @{const_syntax If} $ freetest $
            update_tr ctxt [] offset offset new var g' $
            update_tr ctxt [] offset offset Null var (Bound 0);

      in Syntax.const @{const_syntax Basic} $ Abs ("s", dummyT, cond)
      end
  | new_tr _ ts = raise TERM ("new_tr",ts);

fun nnew_tr ctxt (ts as [var,size,init]) =
      let
        fun offset v = 0;
        fun dest_init (Const (@{syntax_const "_newinit"}, _) $ Const (var, _) $ v) = (var, v)
          | dest_init _ = raise Match;

        fun dest_inits (Const (@{syntax_const "_newinits"}, _) $ x $ xs) =
              dest_init x :: dest_inits xs
          | dest_inits (t as (Const (@{syntax_const "_newinit"}, _) $ _ $ _)) =
              [dest_init t]
          | dest_inits _ = raise Match;

        val g = Syntax.free globalsN $ Bound 0;
        val alloc = lookup_comp ctxt [] allocN (Bound 0);
        val new = Syntax.free "new" $ (Syntax.const @{const_syntax set} $ alloc);  (* fixme new !? *)

        fun mk_upd (var,v) =
          let
            val varn = Hoare.varname var;
            val var' = lookup_comp ctxt [] varn (Bound 0);
          in
            update_comp ctxt NONE [] false false varn
              (Syntax.const @{const_syntax fun_upd} $ var' $ new $ v)
          end;

        val inits = map mk_upd (dest_inits init);
        val free = lookup_comp ctxt [] freeN (Bound 0);
        val freetest = Syntax.const @{const_syntax Orderings.less_eq} $ size $ free;

        val alloc_upd =
          update_comp ctxt NONE [] false false allocN
            (Syntax.const @{const_syntax Cons} $ new $ alloc);
        val free_upd =
          update_comp ctxt NONE [] false false freeN
            (Syntax.const @{const_syntax Groups.minus} $ free $ size);

        val g' =
          Syntax.free (suffix Record.updateN globalsN) $
            K_rec_syntax (fold (fn upd => fn s => upd s) (alloc_upd :: inits @ [free_upd]) g) $
            Bound 0;
        val cond =
          Syntax.const @{const_syntax if_rel} $ Abs ("s", dummyT, freetest) $
            Abs ("s", dummyT, update_tr ctxt [] offset offset new var g') $
            Abs ("s", dummyT, update_tr ctxt [] offset offset Null var (Bound 0)) $
            Abs ("s", dummyT, update_tr ctxt [] offset offset new var g');

      in Syntax.const @{const_syntax Spec} $ cond
      end
  | nnew_tr _ ts = raise TERM ("nnew_tr", ts);

fun loc_tr ctxt (ts as [init, bdy]) =
  let
    fun dest_init (Const (@{syntax_const "_locinit"}, _) $ Const (var,_) $ v) = (var, v)
      | dest_init (Const (@{syntax_const "_locnoinit"}, _) $ Const (var, _)) =
           (var, Syntax.const antiquoteCur $ Syntax.free (Hoare.varname var))
           (* fixme: could skip this dummy initialisation v := v s and
              derive non init variables in the print translation from
              the return function instead the init function *)
      | dest_init _ = raise Match;

    fun dest_inits (Const (@{syntax_const "_locinits"}, _) $ x $ xs) = dest_init x :: dest_inits xs
      | dest_inits (t as (Const (@{syntax_const "_locinit"}, _) $ _ $ _)) = [dest_init t]
      | dest_inits (t as (Const (@{syntax_const "_locnoinit"}, _) $ _)) = [dest_init t]
      | dest_inits _ = raise Match;

    fun mk_init_upd (var, v) =
      update_comp ctxt NONE [] true false var (antiquoteCur_tr ctxt v);

    fun mk_ret_upd var =
      update_comp ctxt NONE [] true false var (lookup_comp ctxt [] var (Bound 1));

    val var_vals = map (apfst Hoare.varname) (dest_inits init);
    val ini = Abs ("s", dummyT, fold mk_init_upd var_vals (Bound 0));
    val ret = Abs ("s",dummyT, Abs ("t",dummyT, fold (mk_ret_upd o fst) var_vals (Bound 0)));
    val c = Abs ("i", dummyT, Abs ("t", dummyT, Syntax.const @{const_syntax Skip}));

  in Syntax.const @{const_syntax block} $ ini $ bdy $ ret $ c end

infixr 9 &;

fun (NONE & NONE) = NONE
  | ((SOME x) & NONE) = SOME x
  | (NONE & (SOME x)) = SOME x
  | ((SOME x) & (SOME y)) = SOME (Syntax.const @{const_syntax HOL.conj} $ x $ y);

fun mk_imp (l,SOME r) = SOME (HOLogic.mk_imp (l, r))
  | mk_imp (l,NONE) = NONE;


local

fun le l r =
  Syntax.const @{const_syntax Orderings.less} $ l $ r;

fun in_range t = Syntax.free "in_range" $ t;   (* fixme ?? *)

fun not_zero t =
  Syntax.const @{const_syntax Not} $
    (Syntax.const @{const_syntax HOL.eq} $ t $ Syntax.const @{const_syntax Groups.zero});

fun not_Null t =
  Syntax.const @{const_syntax Not} $
    (Syntax.const @{const_syntax HOL.eq} $ t $ Syntax.free "Simpl_Heap.Null");   (* fixme ?? *)

fun in_length i l =
  Syntax.const @{const_syntax Orderings.less} $ i $
    (Syntax.const @{const_syntax size} $ l);

fun is_pos t =
  Syntax.const @{const_syntax Orderings.less_eq} $ Syntax.const @{const_syntax Groups.zero} $ t;


fun infer_type ctxt t =
  Syntax.check_term ctxt (Exn.release (#2 (Syntax_Phases.decode_term ctxt ([], Exn.Res t))));


(* NOTE: operations on actual terms *)

fun is_arr (Const (@{const_name List.nth},_) $ l $ e) = is_arr l
  | is_arr (Const (a, _) $ Bound 0) = Hoare.is_state_var a
  | is_arr (Const (a,_) $ (Const (globals,_) $ Bound 0)) = Hoare.is_state_var a
  | is_arr ((Const (hp,_) $ (Const (globals,_) $ Bound 0)) $ p) = Hoare.is_state_var hp
  | is_arr _ = false;

fun dummyfyT (TFree x) = TFree x
  | dummyfyT (TVar x) = dummyT
  | dummyfyT (Type (c, Ts)) =
     let
       val Ts' = map dummyfyT Ts;
     in if exists (fn T => T = dummyT) Ts' then dummyT else Type (c, Ts') end;

fun guard ctxt Ts (add as (Const (@{const_name Groups.plus},_) $ l $ r)) =
      guard ctxt Ts l & guard ctxt Ts r & SOME (in_range add)
  | guard ctxt Ts (sub as (Const (@{const_name Groups.minus},_) $ l $ r)) =
      let
        val g =
          (if fastype_of1 (Ts,sub) = HOLogic.natT then le r l else in_range sub)
            handle TERM _ => error ("guard generation, cannot determine type of: " ^
              Syntax.string_of_term ctxt sub);
      in guard ctxt Ts l & guard ctxt Ts r & SOME g end
  | guard ctxt Ts (mul as (Const (@{const_name Groups.times},_) $ l $r)) =
      guard ctxt Ts l & guard ctxt Ts r & SOME (in_range mul)
  | guard ctxt Ts (Const (@{const_name HOL.conj},_) $ l $ r) =
      guard ctxt Ts l & mk_imp (l,guard ctxt Ts r)
  | guard ctxt Ts (Const (@{const_name HOL.disj},_) $ l $ r) =
      guard ctxt Ts l & mk_imp (HOLogic.Not $ l,guard ctxt Ts r)
  | guard ctxt Ts (dv as (Const (@{const_name Rings.divide},_) $ l $ r)) =
      guard ctxt Ts l & guard ctxt Ts r & SOME (not_zero r) & SOME (in_range dv) (* fixme: Make more concrete guard...*)
  | guard ctxt Ts (Const (@{const_name Rings.modulo},_) $ l $ r) =
      guard ctxt Ts l & guard ctxt Ts r & SOME (not_zero r)
  | guard ctxt Ts (un as (Const (@{const_name Groups.uminus},_) $ n)) =
      guard ctxt Ts n & SOME (in_range un)
  | guard ctxt Ts (Const (@{const_name Int.nat},_) $ i) =
      guard ctxt Ts i & SOME (is_pos i)
  | guard ctxt Ts (i as (Const (@{const_abbrev Int.int},_) $ n)) =
      guard ctxt Ts n & SOME (in_range i)
  | guard ctxt Ts (Const (@{const_name List.nth},_) $ l $ e) =
      if is_arr l then guard ctxt Ts l & guard ctxt Ts e & SOME (in_length e l)
      else NONE (*oder default?*)
  | guard ctxt Ts (Const (hp,_) $ (Const (globals,_) $ Bound 0) $ p) =
      if Hoare.is_state_var hp then guard ctxt Ts p & SOME (not_Null p)(*& SOME (in_alloc p)*)
      else guard ctxt Ts p

(*  | guard (Const (@{const_name "list_update"},_)$l$i$e) =
      if is_arr l then guard i & SOME (in_length i l) & guard e else NONE*) (* oder default?*)
(*  | guard (Const (upd,_)$e$s) = for procedure parameters,like default but left to right
      if is_some (try (unsuffix updateN) upd) then guard s & guard e else guard e & guard s *)
  | guard ctxt Ts t =
      fold_rev (fn l => fn r => guard ctxt Ts l & r) (snd (strip_comb t)) NONE (* default *)
  | guard _ _ _ = NONE;

in

 fun mk_guard ctxt t =
   let
      (* We apply type inference first, so that we can generate different guards,
         depending on the type, e.g. int vs. nat *)
      val Abs (_, T, t') = map_types dummyfyT (infer_type ctxt (Abs ("s", dummyT, t)));
   in guard ctxt [T] t' end;

end;
(* fixme: make guard function a parameter of all parse-translations that need it.*)

val _ = Theory.setup (Context.theory_map (Hoare.install_generate_guard mk_guard));


fun mk_singleton_guard f g =
  Syntax.const @{const_syntax Cons} $
    (Syntax.const @{const_syntax Pair} $ Syntax.const f $
      (Syntax.const @{const_syntax Collect} $ Abs ("s", dummyT, g))) $
    Syntax.const @{const_syntax Nil};

fun guarded_Assign_tr ctxt (ts as [v, e]) =
      let
        val ass = assign_tr ctxt [v, e];
        val guard = Hoare.generate_guard ctxt;
        (* By the artificial "=" between left and right-hand side we get a bigger term and thus
           more information for type-inference *)
      in
        case guard (Syntax.const @{const_syntax HOL.eq} $
            antiquoteCur_tr ctxt v $ antiquoteCur_tr ctxt e) of
          NONE => ass
        | SOME g =>
            Syntax.const @{const_syntax guards} $ mk_singleton_guard @{const_syntax False} g $ ass
      end
  | guarded_Assign_tr _ ts = raise Match;

fun guarded_New_tr ctxt (ts as [var, size, init]) =
      let
        val new = new_tr ctxt [var, size, init];
        val guard = Hoare.generate_guard ctxt;
      in
        case guard (antiquoteCur_tr ctxt var) of
          NONE => new
        | SOME g =>
            Syntax.const @{const_syntax guards} $ mk_singleton_guard @{const_syntax False} g $ new
      end
  | guarded_New_tr _ ts = raise TERM ("guarded_New_tr", ts);

fun guarded_NNew_tr ctxt (ts as [var, size, init]) =
      let
        val new = nnew_tr ctxt [var, size, init];
        val guard = Hoare.generate_guard ctxt;
      in
        case guard (antiquoteCur_tr ctxt var) of
          NONE => new
        | SOME g =>
            Syntax.const @{const_syntax guards} $ mk_singleton_guard @{const_syntax False} g $ new
      end
  | guarded_NNew_tr _ ts = raise TERM ("guarded_NNew_tr", ts);


fun guarded_While_tr ctxt (ts as [b,I,V,c]) =
      let
        val guard = Hoare.generate_guard ctxt;
        val cnd as Abs (_, _, b') = quote_tr ctxt antiquoteCur b;
        val b'' = Syntax.const @{const_syntax Collect} $ cnd;
      in
        case guard b' of
          NONE => Syntax.const @{const_syntax whileAnno} $ b'' $ I $ V $ c
        | SOME g =>
            Syntax.const @{const_syntax whileAnnoG} $
              mk_singleton_guard @{const_syntax False} g $ b'' $ I $ V $ c
      end
  | guarded_While_tr _ ts = raise Match;

fun guarded_WhileFix_tr ctxt (ts as [b as (_ $ Abs (_, _, b')), I, V, c]) =
      let
        val guard = Hoare.generate_guard ctxt;
      in
        case guard b' of
          NONE => Syntax.const @{const_syntax whileAnnoFix} $ b $ I $ V $ c
        | SOME g =>
            Syntax.const @{const_syntax whileAnnoGFix} $
              mk_singleton_guard @{const_syntax False} g $ b $ I $ V $ c
      end
  | guarded_WhileFix_tr _ ts = raise Match;

fun guarded_Cond_tr ctxt (ts as [b, c, d]) =
      let
        val guard = Hoare.generate_guard ctxt;
        val cnd as Abs (_, _, b') = quote_tr ctxt @{syntax_const "_antiquoteCur"} b;
        val cond =
          Syntax.const @{const_syntax Cond} $ (Syntax.const @{const_syntax Collect} $ cnd) $ c $ d;
      in
        case guard b' of
          NONE => cond
        | SOME g =>
            Syntax.const @{const_syntax guards} $ mk_singleton_guard @{const_syntax False} g $ cond
      end
  | guarded_Cond_tr _ ts = raise Match;


(* parsing procedure calls *)

fun dest_pars (Const (@{syntax_const "_par"}, _) $ p) = [p]
  | dest_pars (Const (@{syntax_const "_pars"}, _) $ p $ ps) = dest_pars p @ dest_pars ps
  | dest_pars t = raise TERM ("dest_pars", [t]);

fun dest_actuals (Const (@{syntax_const "_actuals_empty"}, _)) = []
  | dest_actuals (Const (@{syntax_const "_actuals"}, _) $ pars) = dest_pars pars
  | dest_actuals t = raise TERM ("dest_actuals", [t]);


fun mk_call_tr ctxt grd Call formals pn pt actuals has_args result_exn cont =
  let
    val fcall = cont <> NONE;
    val state_kind =
      the_default (Hoare.get_default_state_kind ctxt)
        (Hoare.get_state_kind pn ctxt);
    fun init_par_tr name lense_opt arg =
      update_comp ctxt lense_opt [] false false name (antiquoteCur_tr ctxt arg);

    fun result_par_tr name arg =
      let
        fun offset_old n = 2;
        fun offset n = if is_global ctxt n then 0 else 2;
        val lookup = lookup_comp ctxt [] name (Bound 1)
      in
        update_tr ctxt [pn] offset offset_old lookup arg
      end;

    val _ = if not (Config.get ctxt StateSpace.silent) andalso
               ((not fcall andalso length formals <> length actuals)
                 orelse
                (fcall andalso length formals <> length actuals + 1))
            then raise
                TERM ("call_tr: number of formal (" ^ string_of_int (length formals) ^
                      ") and actual (" ^ string_of_int (length actuals) ^
                      ") parameters for \"" ^ unsuffix Hoare.proc_deco pn ^
                      "\" do not match.", [])
            else ();

    val globals =
      [Syntax.const globals_updateN $ (K_rec_syntax (Const (globalsN, dummyT) $ Bound 0))];
    val ret = Abs ("s", dummyT, Abs ("t", dummyT, Library.foldr (op $) (globals, Bound 1)));

    val val_formals = filter (fn (kind, _, _) => kind = Hoare.In) formals;
    val res_formals = filter (fn (kind, _, _) => kind = Hoare.Out) formals;

    val (val_actuals, res_actuals) = chop (length val_formals) actuals;
    val init_bdy =
      let
        val state =
          (case state_kind of
            Hoare.Record => Bound 0
          | _ => Syntax.const localsN $ Bound 0);
        val upds = fold2 (fn (_, name, lense_opt) => init_par_tr name lense_opt) val_formals val_actuals state;
      in
        (case state_kind of
          Hoare.Record => upds
        | _ => Syntax.const locals_updateN $ K_rec_syntax upds $ Bound 0)
      end;
    val init = Abs ("s", dummyT, init_bdy);


    val call =
      (case cont of
        NONE => (* Procedure call *)
            let
              val results =
                map (fn ((_, name, _), arg) => result_par_tr name arg)
                  (rev (res_formals ~~ res_actuals));
              val res =
                Abs ("i", dummyT, Abs ("t", dummyT,
                    Syntax.const @{const_syntax Basic} $
                      Abs ("s", dummyT, fold_rev (fn f => fn s => f s) results (Bound 0))));
              val args = [init, pt, ret] @ result_exn @ [res]
            in if has_args then list_comb (Call, args) else Call $ pt end
        | SOME c => (* Function call *)
            let
              val res =
                (case res_formals of
                  [(_, n, _)] => Abs ("s", dummyT, lookup_comp ctxt [] n (Bound 0))
                | _ =>
                    if Config.get ctxt StateSpace.silent
                    then Abs ("s", dummyT, lookup_comp ctxt [] "dummy" (Bound 0))
                    else raise TERM ("call_tr: function " ^ pn ^ "may only have one result parameter", []));
            in Call $ init $ pt $ ret $ res $ c end)
    val guard = Hoare.generate_guard  ctxt;
  in
    if grd
    then
      (case fold_rev (fn arg => fn g => guard (antiquoteCur_tr ctxt arg) & g)
          (res_actuals @ val_actuals) NONE of
        NONE => call
      | SOME g =>
          Syntax.const @{const_syntax guards} $ mk_singleton_guard @{const_syntax False} g $ call)
    else call
  end;


fun dest_procname ctxt false (Const (p, _)) =
      (suffix Hoare.proc_deco p, HOLogic.mk_string p)
  | dest_procname ctxt false (t as Free (p, T)) =
      (case Hoare.get_default_state_space ctxt of
        SOME {read_function_name, ...} => (p, read_function_name ctxt p)
      | _ => (suffix Hoare.proc_deco p, Free (suffix Hoare.proc_deco p, T)))
  | dest_procname ctxt false (Const (@{syntax_const "_free"},_) $ Free (p,T)) =
      (suffix Hoare.proc_deco p, Free (suffix Hoare.proc_deco p, T))
  | dest_procname ctxt false (t as (Const (@{syntax_const "_antiquoteCur"},_) $ Const (p, _))) =
      (Hoare.resuffix Hoare.deco Hoare.proc_deco p, t)
  | dest_procname ctxt false (t as (Const (@{syntax_const "_antiquoteCur"}, _) $ Free (p, _))) =
      (Hoare.resuffix Hoare.deco Hoare.proc_deco p, t)
  | dest_procname ctxt false (t as Const (p, _) $ _) =
      (Hoare.resuffix Hoare.deco Hoare.proc_deco p, t) (* antiquoteOld *)
  | dest_procname ctxt false (t as Free (p,_)$_)  =
      (Hoare.resuffix Hoare.deco Hoare.proc_deco p, t) (* antiquoteOld *)
  | dest_procname ctxt false (t as Const (@{syntax_const "_antiquoteOld"}, _) $ _ $ Const (p, _)) =
      (suffix Hoare.proc_deco p, t)
  | dest_procname ctxt false (t as Const (@{syntax_const "_antiquoteOld"}, _) $ _ $ Free (p,_)) =
      (suffix Hoare.proc_deco p, t)
  | dest_procname ctxt false (t as Const (@{const_name "StateFun.lookup"}, _) $ _ $ Free (p, _) $ _) =
      (suffix Hoare.proc_deco (Hoare.remdeco' ctxt p), t) (* antiquoteOld *)

  | dest_procname ctxt false t = ("", t)
  | dest_procname ctxt true t =
      let fun quote t = Abs ("s", dummyT, antiquoteCur_tr ctxt t)
      in
        (case quote t of
          (t' as Abs (_, _, Free (p, _) $ Bound 0)) =>
            (Hoare.resuffix Hoare.deco Hoare.proc_deco p, t')
        | (t' as Abs (_, _, Const (@{const_name "StateFun.lookup"}, _) $ _ $ Free (p, _) $ (_ $ Bound 0))) =>
            (suffix Hoare.proc_deco (Hoare.remdeco' ctxt p), t')
        | t' => ("", t'))
      end

fun gen_call_tr dyn grd ctxt p actuals has_args result_exn cont =
  let
    fun Call false true [] NONE = Const (@{const_syntax call}, dummyT)
      | Call false true _ NONE = Const (@{const_syntax call_exn}, dummyT)
      | Call false false [] NONE = Const (@{const_syntax Call}, dummyT)
      | Call true true [] NONE = Const (@{const_syntax dynCall}, dummyT)
      | Call true true _ NONE = Const (@{const_syntax dynCall_exn}, dummyT)
      | Call false true [] (SOME c) = Const (@{const_syntax fcall}, dummyT)
      | Call _ _ _ _ = raise TERM ("gen_call_tr: no proper procedure call", []);

    val (pn, pt) = dest_procname ctxt dyn (Term_Position.strip_positions p);
  in
    (case Hoare.get_params pn ctxt of
      SOME formals =>
        mk_call_tr ctxt grd (Call dyn has_args result_exn cont) formals pn pt actuals has_args result_exn cont
    | NONE =>
        if Config.get ctxt StateSpace.silent
        then mk_call_tr ctxt grd (Call dyn has_args result_exn cont) [] pn pt [] has_args result_exn cont
        else raise TERM ("gen_call_tr: procedure " ^ quote pn ^ " not defined", []))
  end;

fun call_tr dyn grd result_exn ctxt [p, actuals] =
      gen_call_tr dyn grd ctxt p (dest_actuals actuals) true result_exn NONE
  | call_tr _ _ _ _ t = raise TERM ("call_tr", t);

fun call_ass_tr dyn grd result_exn ctxt [l, p, actuals] =
      gen_call_tr dyn grd ctxt p (dest_actuals actuals @ [l]) true result_exn NONE
  | call_ass_tr  _ _ _ _ t = raise TERM ("call_ass_tr", t);

fun proc_tr ctxt [p, actuals] =
      gen_call_tr false false ctxt p (dest_actuals actuals) false [] NONE
  | proc_tr _  t = raise TERM ("proc_tr", t);

fun proc_ass_tr ctxt [l, p, actuals] =
      gen_call_tr false false ctxt p (dest_actuals actuals @ [l]) false [] NONE
  | proc_ass_tr _ t = raise TERM ("proc_ass_tr", t);

fun fcall_tr ctxt [p, actuals, c] =
      gen_call_tr false false ctxt p (dest_actuals actuals) true [] (SOME c)
  | fcall_tr _ t = raise TERM ("fcall_tr", t);


(* printing procedure calls *)

fun upd_tr' ctxt (x_upd, T) =
  (case try (unsuffix' Record.updateN) x_upd of
    SOME x =>
      (Hoare.chopsfx Hoare.deco (Hoare.extern ctxt x),
       if T = dummyT then T else Term.domain_type T)
  | NONE =>
      (case try (unsuffix Hoare.deco) x_upd of
        SOME _ => (Hoare.remdeco ctxt x_upd, T)
      | NONE => raise Match));


fun update_name_tr' ctxt (Free x) = Const (upd_tr' ctxt x)
  | update_name_tr' ctxt ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
      (*c $*) Const (upd_tr' ctxt x)
  | update_name_tr' ctxt (Const x) = Const (upd_tr' ctxt x)
  | update_name_tr' ctxt t =
     (case Hoare.get_default_state_space ctxt of
       SOME {update_tr',...} => update_tr' ctxt t
     | NONE => raise Match);


fun term_name_eq (Const (x, _)) (Const (y, _)) = (x = y)
  | term_name_eq (Free (x, _)) (Free (y, _)) = (x = y)
  | term_name_eq (Var (x, _)) (Var (y, _)) = (x = y)
  | term_name_eq (a $ b) (c $ d) = term_name_eq a c andalso term_name_eq b d
  | term_name_eq (Abs (s, _, a)) (Abs (t, _, b)) = (s = t) andalso term_name_eq a b
  | term_name_eq _ _ = false;

fun list_update_tr' l (r as Const (@{const_syntax list_update},_) $ l' $ i $ e) =
      if term_name_eq l l'
      then
        let
          fun sel_arr a [i] (Const (@{const_syntax nth},_) $ a' $ i') =
                term_name_eq a a' andalso i = i'
            | sel_arr a (i::is) (Const (@{const_syntax nth},_) $ sel $ i') =
                i = i' andalso sel_arr a is sel
            | sel_arr _ _ _ = false;

          fun tr' a idxs (e as Const (@{const_syntax list_update}, _) $ sel $ i $ e') =
                if sel_arr a idxs sel then tr' a (i :: idxs) e'
                else (idxs, e)
            | tr' _ idxs e = (idxs, e);

          val (idxs, e') = tr' l [i] e;
          val lft = fold_rev (fn i => fn arr => Syntax.const @{const_syntax nth} $ arr $ i) idxs l;
        in (lft,e') end
      else (l, r)
  | list_update_tr' l r  = (l, r);

fun list_mult_update_tr' l (r as Const (@{const_syntax list_multupd},_) $ var $ idxs $ values) =
      (Syntax.const @{const_syntax list_multsel} $ var $ idxs, values)
  | list_mult_update_tr' l r = (l, r);

fun update_tr' ctxt l (r as Const (@{const_syntax fun_upd}, _) $
        (hp as (Const (@{syntax_const "_antiquoteCur"}, _) $ _)) $ p $ value) =
      if term_name_eq l hp then
        (case value of
          (Const (@{const_syntax list_update}, _) $ _ $ _ $ _) => list_update_tr' (l $ p) value
        | (Const (@{const_syntax list_multupd},_) $ _ $ _ $ _) => list_mult_update_tr' (l $ p) value
        | _ => (l $ p, value))
      else (l, r)
  | update_tr' ctxt l (r as Const (@{const_syntax list_update},_) $
        (var as (Const (@{syntax_const "_antiquoteCur"}, _) $ _)) $ i $ value) =
      if term_name_eq l var then list_update_tr' l r else (l, r)
  | update_tr' ctxt l (r as Const (@{const_syntax list_multupd}, _) $
        (var as (Const (@{syntax_const "_antiquoteCur"}, _) $ _)) $ idxs $ values) =
      if term_name_eq l var then list_mult_update_tr' l r else (l, r)
  | update_tr' ctxt l r = (l, r);


fun dest_K_rec (Abs (_, _, Abs (_, _, v) $ Bound 0)) = (* eta expanded version *)
      let val lbv = loose_bnos v;
      in if member (op =) lbv 0 orelse member (op =) lbv 1
         then NONE else SOME (incr_boundvars ~2 v)
      end
  | dest_K_rec (Abs (_, _, v)) =
      if member (op =) (loose_bnos v) 0 then NONE else SOME (incr_boundvars ~1 v)
  | dest_K_rec (Const (@{const_syntax K_statefun}, _) $ v) = SOME v
  | dest_K_rec _ = NONE;

fun the_Match (SOME x) = x
  | the_Match (NONE) = raise Match

fun dest_update ctxt (upd' $ dest $ constr $ n $ v $ s) =
      (n, v, SOME s)
  | dest_update ctxt (upd' $ dest $ constr $ n $ v) =
      (n, v, NONE)
  | dest_update ctxt t =
     case Hoare.get_default_state_space ctxt of
       SOME {dest_update_tr', ...} => dest_update_tr' ctxt t
     | NONE => raise Match

local
fun uncover ctxt (upd,v) = (upd, v) |> first_match [
  fn (Const (cupd, _), t) =>
      if member (op =) [globals_updateN, locals_updateN] (Long_Name.base_name cupd)
      then case dest_update ctxt t of
             (n, v', SOME s) => (case s of (Const (g, _) $ _) =>
                                   if member (op =) [localsN, globalsN] (Long_Name.base_name g)
                                   then (n, the_Match (dest_K_rec v'))
                                   else raise Match
                                 | _ => raise Match)
           | (n, v', NONE) => (n, the_Match (dest_K_rec v'))
      else (upd, v),
  fn (upd, v ) =>
    (case (upd, v) of
      (Const (gupd, _), t as (upd' $ k $ s)) =>
        (case dest_K_rec k of
          SOME v' =>
            if Long_Name.base_name gupd = globals_updateN
            then
              (case s of
                Const (gl, _) $ _ =>
                  if Long_Name.base_name gl = globalsN (* assignment *)
                  then (upd',v')
                  else raise Match
              | _ => raise Match)
            else (upd, v)
        | _ => (upd, v))
    | (Const (upd_glob, _), upd' $ v') =>
        if Long_Name.base_name upd_glob = upd_globalsN (* result parameter *)
        then (upd', v')
        else if Long_Name.base_name upd_glob = globals_updateN
          then (case dest_K_rec v' of
                  SOME v'' => (upd',v'')
                | _ => (upd, v))
          else (upd, v)
    | _ => (upd, v))]
in

fun global_upd_tr' ctxt upd k =
  (case dest_K_rec k of
    SOME v => uncover ctxt (upd, v)
  | NONE => uncover ctxt (upd, k))
end;

fun dest_updates ctxt t = t |> first_match [
  fn (t as (upd as Const (u, _)) $ k $ state) =>
      (case dest_K_rec k of
        SOME value =>
          if member (op =) [globals_updateN, locals_updateN] (Long_Name.base_name u)
          then dest_updates ctxt value
          else if can (unsuffix Record.updateN) u orelse Long_Name.base_name u = upd_globalsN
          then (upd,value)::dest_updates ctxt state
          else raise Match
      | NONE => raise Match (*dest_updates ctxt k @ dest_updates ctxt state*) (* check for nested update (e.g. locals-stack) *)
                (*handle Match => []*)), (* t could be just (globals $ s) *)
  fn (t as (upd as Const (u,_))$k) =>
      (case dest_K_rec k of
        SOME value =>
          if member (op =) [globals_updateN, locals_updateN] (Long_Name.base_name u)
          then dest_updates ctxt value
          else if can (unsuffix Record.updateN) u orelse Long_Name.base_name u = upd_globalsN
          then [(upd,value)]
          else if Long_Name.base_name u = globalsN then [] else raise Match
      | NONE => dest_updates ctxt k (* check for nested update (e.g. locals-stack) *)
                handle Match => []), (* t could be just (globals $ s) *)
  fn ((Const (u, _)) $ _ $ _ $ n $ k $ state) =>
      if Long_Name.base_name u = Long_Name.base_name StateFun.updateN
      then case dest_K_rec k of SOME value => (n, value) :: dest_updates ctxt state | _ => raise Match
      else raise Match,
  fn ((Const (u, _)) $ _ $ _ $ n $ k) =>
      if Long_Name.base_name u = Long_Name.base_name StateFun.updateN
      then case dest_K_rec k of SOME value => [(n, value)] | _ => raise Match
      else raise Match,
  fn t =>
       (case Hoare.get_default_state_space ctxt of
          SOME {dest_update_tr', ...} =>
            (case dest_update_tr' ctxt t of
               (n, v, SOME s) => (n, the_Match (dest_K_rec v))::dest_updates ctxt s
             | (n, v, NONE) => [(n, the_Match (dest_K_rec v))])
        | NONE => raise Match),
  fn t => []]

fun dest_updates ctxt t = t |> first_match [
  fn (t as (upd as Const (u, _)) $ k $ state) =>
       if member (op =) [globals_updateN, locals_updateN] (Long_Name.base_name u) then
          dest_updates ctxt k @ dest_updates ctxt state
       else if can (unsuffix Record.updateN) u orelse Long_Name.base_name u = upd_globalsN then
          (upd, the_Match (dest_K_rec k))::dest_updates ctxt state
       else raise Match, (* t could be just (globals $ s) *)
  fn (t as (upd as Const (u,_))$k) =>
       if member (op =) [globals_updateN, locals_updateN] (Long_Name.base_name u) then
         dest_updates ctxt k
       else if can (unsuffix Record.updateN) u orelse Long_Name.base_name u = upd_globalsN then
         [(upd, the_Match (dest_K_rec k))]
       (*else if Long_Name.base_name u = globalsN then [] *)
       else raise Match,
  fn ((Const (u, _)) $ _ $ _ $ n $ k $ state) =>
       if Long_Name.base_name u = Long_Name.base_name StateFun.updateN then
         (n, the_Match (dest_K_rec k)) :: dest_updates ctxt state
       else raise Match,
  fn ((Const (u, _)) $ _ $ _ $ n $ k) =>
      if Long_Name.base_name u = Long_Name.base_name StateFun.updateN then
        [(n, the_Match (dest_K_rec k))]
      else raise Match,
  fn t =>
       (case Hoare.get_default_state_space ctxt of
          SOME {dest_update_tr', ...} =>
            (case dest_update_tr' ctxt t of
               (n, v, SOME s) => (n, the_Match (dest_K_rec v))::dest_updates ctxt s
             | (n, v, NONE) => [(n, the_Match (dest_K_rec v))])
        | NONE => raise Match),
  fn t => []]


(* fixme: externalize names properly before removing decoration! *)
fun init_tr' ctxt [Abs (_,_,t)] =
  let
    val upds  =
      case dest_updates ctxt t of
        us as [(Const (gupd, _), v)] =>
          if Long_Name.base_name gupd = globals_updateN
          then dest_updates ctxt v else us
      | us => us;

    val comps =
      map (fn (Const (u, _)) => Symbol.explode (unsuffix (Hoare.deco ^ Record.updateN) u))
        (map fst upds);
    val prfx = maxprefixs (op =) comps;

    fun dest_list (Const (@{const_syntax Nil}, _)) = []
      | dest_list (Const (@{const_syntax Cons}, _) $ x $ xs) = x :: dest_list xs
      | dest_list t = [t];

    fun mk_set [] = Syntax.const @{const_syntax Set.empty}
      | mk_set (x :: xs) = Syntax.const @{const_syntax insert} $ x $ mk_set xs;

    val l = length prfx;
    val _ = if l <= 1 then raise Match else ();
    val comp = mk_list (map (Syntax.const o implode o drop l) comps);
    val vals = map mk_set (transpose (map (dest_list o snd) upds));
    val v = case vals of [v] => v | vs => mk_list vs;
  in
    Syntax.const @{syntax_const "_Init"} $
      Syntax.const (implode (fst (split_last prfx))) $ comp $ v
  end;


local
fun tr' ctxt c (upd,v) =
  let
    val l = Syntax.const antiquoteCur $ update_name_tr' ctxt upd;
    val r = quote_tr' ctxt antiquoteCur (Abs ("s", dummyT, v));
    val (l', r') = update_tr' ctxt l r;
  in (c $ l' $ r') end;

in
fun app_assign_tr' c ctxt (Abs (s, _, upd $ v $ Bound 0) :: ts) =
      tr' ctxt c (global_upd_tr' ctxt upd v)
  | app_assign_tr' c ctxt ((upd $ v) :: ts) =
      (case upd of
        u $ v => raise Match
      | _ => tr' ctxt c (global_upd_tr' ctxt upd v))
  | app_assign_tr' _ _ _ = raise Match;
end;

val assign_tr' = app_assign_tr' (Syntax.const @{syntax_const "_Assign"});
val raise_tr' = app_assign_tr' (Syntax.const @{syntax_const "_raise"});

fun split_Let' ((l as Const (@{const_syntax Let'}, _)) $ x $ t) =
      let val (recomb,t') = split_Let' t
      in (fn t => l $ x $ recomb t, t') end
  | split_Let' (Abs (x, T, t)) =
     let val (recomb, t') = split_Let' t
     in if t' = t
        then (I, t') (* Get rid of last abstraction *)
        else (fn t => Abs (x, T, recomb t), t')
     end
  | split_Let' ((s as Const (@{const_syntax case_prod},_)) $ t) =
     let val (recomb, t') = split_Let' t
     in (fn t => s $ recomb t, t') end
  | split_Let' t = (I, t)

fun basic_tr' ctxt [Abs (s, T, t)] =
  let
    val (has_let, t') =
      case t of
        ((t' as (Const (@{const_syntax Let'},_) $ _ $ _)) $ Bound 0) => (true, t')
      | _ => (false, t);
    val (recomb, t'') = split_Let' t';
    val upds = dest_updates ctxt t'';
    val _ = if length upds <= 1 andalso not has_let then raise Match else ();
    val ass =
      map (fn (u, v) => app_assign_tr' (Syntax.const @{syntax_const "_BAssign"}) ctxt
            [Abs ("s",dummyT,u$v$Bound 0)]) upds;
    val basics = foldr1 (fn (x, ys) => Syntax.const @{syntax_const "_basics"} $ x $ ys) (rev ass);
  in
    Syntax.const @{syntax_const "_Basic"} $
      quote_tr' ctxt @{syntax_const "_antiquoteCur"} (Abs (s, T, recomb basics))
  end;

fun loc_tr' ctxt [init, bdy, return, c] =
      (let
        val upds =
          (case init of
            Abs (_, _, t as (upd $ v $ s)) => dest_updates ctxt t
          | upd $ v => dest_updates ctxt (upd $ v $ Bound 0)
          | _ => raise Match);

        fun mk_locinit c v =
          Syntax.const @{syntax_const "_locinit"} $
            Syntax.const c $ quote_tr' ctxt antiquoteCur (Abs ("s", dummyT, v));

        fun init_or_not c c' v =
          if c = c' then
            Syntax.const @{syntax_const "_locnoinit"} $ Syntax.const (Hoare.remdeco ctxt c')
          else mk_locinit (Hoare.remdeco ctxt c) v;

        fun mk_init (Const (c, _), (v as (Const (c', _) $ Bound 0))) =
              init_or_not (unsuffix' Record.updateN c) c' v
          | mk_init (Const (c, _), v) =
              mk_locinit (unsuffix' (Hoare.deco ^ Record.updateN) (Hoare.extern ctxt c)) v
          | mk_init ((f as Const (@{syntax_const "_free"}, _)) $ Free (c, _), v) =
              (case v of
                Const (lookup, _) $ _ $
                  (Const (@{syntax_const "_free"}, _) $ Free (c', _)) $
                  (Const (locals,_) $ Bound 0) =>
                if Long_Name.base_name lookup = Long_Name.base_name StateFun.lookupN
                  andalso Long_Name.base_name locals = localsN
                then init_or_not c c' v
                else mk_locinit (Hoare.remdeco' ctxt c) v
              | _ => mk_locinit (Hoare.remdeco' ctxt c) v)
          | mk_init _ = raise Match;

        val inits =
          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_locinits"} $ t $ u)
            (map mk_init (rev upds));
      in Syntax.const @{syntax_const "_Loc"} $ inits $ bdy end handle Fail _ => raise Match | Empty => raise Match)
  | loc_tr' _ _ = raise Match;


fun actuals_tr' acts =
  (case acts of
    [] => Syntax.const @{syntax_const "_actuals_empty"}
  | xs => Syntax.const @{syntax_const "_actuals"} $
        foldr1 (fn (l, r) => (Syntax.const @{syntax_const "_pars"} $ l $ r)) xs);


fun gen_call_tr' ctxt Call CallAss init p return c =
  let
    fun get_init_updates (Abs (s, _, upds)) = dest_updates ctxt upds
      | get_init_updates upds = dest_updates ctxt upds;

    fun get_res_updates (Abs (i, _, Abs (t, _, Const (@{const_syntax Basic}, _) $ Abs (s, _, upds)))) =
          dest_updates ctxt upds
      | get_res_updates (Abs (i, _, Abs (t, _, Const (@{const_syntax Basic}, _) $ upds))) =
          dest_updates ctxt upds
      | get_res_updates _ = raise Match;

    val init_upds = rev (get_init_updates init)
    fun init_par_tr' par =
        Syntax.const @{syntax_const "_par"} $ quote_tr' ctxt antiquoteCur (Abs ("s", dummyT, par));
    val init_actuals =
      map (fn (_, value) => init_par_tr' value) init_upds;

    fun tr' c (upd, v) =
      let
        val l = Syntax.const antiquoteCur $ update_name_tr' ctxt upd;
        val r =
          quote_tr' ctxt antiquoteCur
            (quote_tr' ctxt antiquoteCur
              (quote_tr' ctxt antiquoteCur
                (Abs ("i", dummyT, Abs ("t", dummyT, Abs ("s", dummyT, v))))));
        val (l', _) = update_tr' ctxt l r;
      in c $ l' end;

    fun ret_par_tr' (upd, v) =
      tr' (Syntax.const @{syntax_const "_par"}) (global_upd_tr' ctxt upd v);

    val res_updates = rev (get_res_updates c);
    val res_actuals = map ret_par_tr' res_updates;
  in
    if Config.get ctxt use_call_tr' then
        (case res_actuals of
          [l] => CallAss $ l $ p $ actuals_tr' init_actuals
         | _ => Call $ p $ actuals_tr' (init_actuals @ res_actuals))
    else raise Match
  end;

fun gen_fcall_tr' ctxt init p return result c =
  let
    fun get_init_updates (Abs (s, _, upds)) = dest_updates ctxt upds
      | get_init_updates _ = raise Match;

    fun init_par_tr' par =
      Syntax.const @{syntax_const "_par"} $ quote_tr' ctxt antiquoteCur (Abs ("s", dummyT, par));
    val init_actuals =
      map (fn (_, value) => init_par_tr' value) (rev (get_init_updates init));

    val (v, c') =
      (case c of
        Abs abs => Syntax_Trans.atomic_abs_tr' ctxt abs
      | _ => raise Match);
  in
    if Config.get ctxt use_call_tr' then
      Syntax.const @{syntax_const "_FCall"} $ p $ actuals_tr' init_actuals $ v $ c'
    else raise Match
  end;


fun pname_tr' ctxt ((f as Const (@{syntax_const "_free"}, _)) $ Free (p, T)) =
      (*f$*) Const (unsuffix' Hoare.proc_deco p, T)
  | pname_tr' ctxt (Free (p, T)) = Const (unsuffix' Hoare.proc_deco p, T)
  | pname_tr' ctxt p =
      let
        (* from HOL strings to ML strings *)
        fun dest_nib c =    (* fixme authentic syntax *)
          (case raw_explode c of
            ["N", "i", "b", "b", "l", "e", h] =>
              if "0" <= h andalso h <= "9" then ord h - ord "0"
              else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
              else raise Match
          | _ => raise Match);

        fun dest_chr (Const (@{const_syntax Char},_) $ Const (c1, _) $ Const (c2,_)) =
              let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2)
              in if Char.isPrint c then c else raise Match end
          | dest_chr _ = raise Match;

        fun dest_string (Const (@{const_syntax Nil}, _)) = []
          | dest_string (Const (@{const_syntax Cons}, _) $ c $ cs) = dest_chr c :: dest_string cs
          | dest_string _ = raise Match;
        in
          (case try dest_string p of
            SOME name => Syntax.const (String.implode name)
          | NONE => antiquote_mult_tr' ctxt (K true) antiquoteCur antiquoteOld p)
        end;

fun call_tr' ctxt [init, p, return, result] =
      gen_call_tr' ctxt
        (Const (@{syntax_const "_Call"}, dummyT))
        (Const (@{syntax_const "_CallAss"}, dummyT)) init (pname_tr' ctxt p) return result
  | call_tr' _ _ = raise Match;

fun call_exn_tr' ctxt [init, p, return, result_exn, result] =
      gen_call_tr' ctxt
        (Const (@{syntax_const "_Call_exn"}, dummyT))
        (Const (@{syntax_const "_CallAss_exn"}, dummyT)) init (pname_tr' ctxt p) return result
  | call_exn_tr' _ _ = raise Match;


fun dyn_call_tr' ctxt [init, p, return, result] =
      let val p' = quote_tr' ctxt antiquoteCur p
      in
        gen_call_tr' ctxt
          (Const (@{syntax_const "_DynCall"}, dummyT))
          (Const (@{syntax_const "_DynCallAss"}, dummyT)) init p' return result
      end
  | dyn_call_tr' _ _ = raise Match;

fun dyn_call_exn_tr' ctxt [init, p, return, result_exn, result] =
      let val p' = quote_tr' ctxt antiquoteCur p
      in
        gen_call_tr' ctxt
          (Const (@{syntax_const "_DynCall_exn"}, dummyT))
          (Const (@{syntax_const "_DynCallAss_exn"}, dummyT)) init p' return result
      end
  | dyn_call_exn_tr' _ _ = raise Match;

fun proc_tr' ctxt [p] =
      let
        val p' = pname_tr' ctxt p;
        val pn = fst (dest_procname ctxt false p');
        val formals = the (Hoare.get_params pn ctxt) handle Option.Option => raise Match;
        val val_formals = map_filter (fn (Hoare.In, p, _) => SOME p | _ => NONE) formals;
        val res_formals = map_filter (fn (Hoare.Out, p, _) => SOME p | _ => NONE) formals;
        fun mkpar n =
          Syntax.const @{syntax_const "_par"} $
            (Syntax.const antiquoteCur $ Syntax.const (Hoare.remdeco ctxt n));
      in
        if not (print_mode_active "NoProc")
        then
          (case res_formals of
            [r] =>
              Syntax.const @{syntax_const "_ProcAss"} $
                (Syntax.const antiquoteCur $
                  Syntax.const (Hoare.remdeco ctxt r)) $
                p' $ actuals_tr' (map mkpar val_formals)
          | _ =>
              Syntax.const @{syntax_const "_Proc"} $ p' $
                actuals_tr' (map mkpar (val_formals @ res_formals)))
         else raise Match
      end
  | proc_tr' _ _ = raise Match;

fun fcall_tr' ctxt [init, p, return, result, c] =
      gen_fcall_tr' ctxt init (pname_tr' ctxt p) return result c
  | fcall_tr' _ _ = raise Match;


(* misc. print translations *)

fun assert_tr' ctxt ((t as Abs (_, _, p)) :: ts) =
      let
        fun selector (Const (c, T)) = Hoare.is_state_var c
          | selector (Const (l, _) $ _ $ _) =
              Long_Name.base_name l = Long_Name.base_name StateFun.lookupN
          | selector t =
              (case Hoare.get_default_state_space ctxt of
                SOME {is_lookup,...} => is_lookup ctxt t
              | _ => false)

        fun fix_state (Const (@{const_syntax HOL.eq},_) $ (Const (@{syntax_const "_free"}, _) $ _)) = true
          | fix_state (Const (@{const_syntax HOL.eq},_) $ (Const (@{syntax_const "_bound"}, _) $ _)) = true
          | fix_state (Const (@{const_syntax HOL.eq},_) $ (Const (@{syntax_const "_var"}, _) $ _)) = true
          | fix_state (Const (@{const_syntax HOL.eq},_) $ Free _) = true
          | fix_state (Const (@{const_syntax HOL.eq},_) $ Bound _) = true
          | fix_state (Const (@{const_syntax HOL.eq},_) $ Var _) = true
          | fix_state _ = false;
      in
        if antiquote_applied_only_to (fn t => selector t orelse fix_state t) p
          andalso not (print_mode_active "NoAssertion")
        then app_quote_mult_tr' ctxt selector (Syntax.const @{syntax_const "_Assert"}) (t :: ts)
        else raise Match
      end
  | assert_tr' _ _ = raise Match


fun bexp_tr' name ctxt ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
      app_quote_tr' ctxt (Syntax.const name) (t :: ts)
  | bexp_tr' _ _ _ = raise Match;



fun new_tr' ctxt
        [Abs (s,_,
          Const (@{const_syntax If}, _) $
          (Const (@{const_syntax Orderings.less_eq},_) $ size $ free) $
          (upd $ new $ (gupd $ Abs (_, _, inits_free_alloc) $ Bound 0)) $
          (upd' $ null $ Bound 0))] =
      let
        fun mk_init (Const (upd, _), Const (@{const_syntax fun_upd},_) $ _ $ _ $ v) =
              let val var = unsuffix' Hoare.deco
                (unsuffix' Record.updateN (Hoare.extern ctxt upd))
              in Syntax.const @{syntax_const "_newinit"} $ Syntax.const var $ v end
          | mk_init ((f as Const (@{syntax_const "_free"}, _)) $
                Free (var, T), Const (@{const_syntax fun_upd},_) $ _ $ _ $ v) =
              Syntax.const @{syntax_const "_newinit"} $
                (f $ Free (Hoare.remdeco' ctxt var, T)) $ v;

        val inits_free_allocs = dest_updates ctxt inits_free_alloc;

        val inits = map mk_init (take (length inits_free_allocs - 2) (inits_free_allocs));
        val inits' =
          foldr1 (fn (t1, t2) => Syntax.const @{syntax_const "_newinits"} $ t1 $ t2) (rev inits);

        fun tr' (upd, v) =
          let
            val l = Syntax.const antiquoteCur $ update_name_tr' ctxt upd;
            val r = quote_tr' ctxt antiquoteCur (Abs (s, dummyT, v));
            val (l', r') = update_tr' ctxt l r
          in l' end;

        val l = tr' (global_upd_tr' ctxt upd' null);

      in Syntax.const @{syntax_const "_New"} $ l $ size $ inits' end
  | new_tr' _ _ = raise Match;

fun nnew_tr' ctxt
        [Const (@{const_syntax if_rel},_) $
          (Abs (s, _, Const (@{const_syntax Orderings.less_eq}, _) $ size $ free)) $
          (Abs (_, _, upd $ new $ (gupd $ (Abs (_, _, free_inits_alloc)) $ Bound 0))) $
          (Abs (_, _, (upd' $ null $ Bound 0))) $ _] =
      let
        fun mk_init (Const (upd, _), Const (@{const_syntax fun_upd}, _) $ _ $ _ $ v) =
              let val var = unsuffix' Hoare.deco
                (unsuffix' Record.updateN (Hoare.extern ctxt upd))
              in Syntax.const @{syntax_const "_newinit"} $ Syntax.const var $ v end
          | mk_init ((f as Const (@{syntax_const "_free"}, _)) $ Free (var, T),
                Const (@{const_syntax fun_upd}, _) $_ $ _ $ v) =
              Syntax.const @{syntax_const "_newinit"} $
                (f $ Free (Hoare.remdeco' ctxt var, T)) $ v;

        val free_inits_allocs = dest_updates ctxt free_inits_alloc;

        val inits = map mk_init (take (length free_inits_allocs - 2) (tl free_inits_allocs));
        val inits' =
          foldr1 (fn (t1, t2) => Syntax.const @{syntax_const "_newinits"} $ t1 $ t2) (rev inits);

        fun tr' (upd, v) =
          let
            val l = Syntax.const antiquoteCur $ update_name_tr' ctxt upd;
            val r = quote_tr' ctxt antiquoteCur (Abs (s, dummyT, v));
            val (l', r') = update_tr' ctxt l r;
          in l' end;

        val l = tr' (global_upd_tr' ctxt upd' null);

      in Syntax.const @{syntax_const "_NNew"} $ l $ size $ inits' end
  | nnew_tr' _ _ = raise Match;


fun switch_tr' ctxt [v, vs] =
  let
    fun case_tr' (Const (@{const_syntax Pair}, _) $ V $ c) =
          Syntax.const @{syntax_const "_switchcase"} $ V $ c
      | case_tr' _ = raise Match;

    fun dest_list (Const (@{const_syntax Nil}, _)) = []
      | dest_list (Const (@{const_syntax Cons}, _) $ x $ xs) = x :: dest_list xs
      | dest_list t = raise Match;

    fun ltr' [] = raise Match
      | ltr' [Vc] = Syntax.const @{syntax_const "_switchcasesSingle"} $ case_tr' Vc
      | ltr' (Vc :: xs) = Syntax.const @{syntax_const "_switchcasesCons"} $ case_tr' Vc $ ltr' xs;

   in app_quote_tr' ctxt (Syntax.const @{syntax_const "_Switch"}) (v :: [ltr' (dest_list vs)]) end;

fun bind_tr' ctxt [e, Abs abs] =
      let
        val (v, c) = Syntax_Trans.atomic_abs_tr' ctxt abs;
        val e' =
          case e of
            Abs a => e
          | t as Const _ => Abs ("s", dummyT, t $ Bound 0)
          | _ => raise Match;
      in app_quote_tr' ctxt (Syntax.const @{syntax_const "_Bind"}) [e', v, c] end
  | bind_tr' _ _ = raise Match;


local
  fun dest_list (Const (@{const_syntax Nil}, _)) = []
    | dest_list (Const (@{const_syntax Cons}, _) $ x $ xs) = x :: dest_list xs
    | dest_list _ = raise Match;

  fun guard_tr' fg =
    let val (flag, g) = HOLogic.dest_prod fg
    in
      if flag aconv @{term True} then Syntax.const @{syntax_const "_guarantee"} $ g
      else if flag aconv @{term False} then g
      else fg
    end handle TERM _ => fg;

  fun guards_lst_tr' [fg] = guard_tr' fg
    | guards_lst_tr' (t :: ts) =
        Syntax.const @{syntax_const "_grds"} $ guard_tr' t $ guards_lst_tr' ts
    | guards_lst_tr' [] = raise Match;

  fun cond_guards_lst_tr' ctxt ts =
    if Config.get ctxt hide_guards then Syntax.const @{syntax_const "_hidden_grds"}
    else guards_lst_tr' ts;
in
  fun guards_tr' ctxt [gs, c] =
        Syntax.const @{syntax_const "_guards"} $ cond_guards_lst_tr' ctxt (dest_list gs) $ c
    | guards_tr' _ _ = raise Match;

  fun whileAnnoG_tr' ctxt [gs, cond as (Const (@{const_syntax Collect}, _) $ b), I, V, c] =
        let
          val b' =
            (case assert_tr' ctxt [b] of
              Const (@{syntax_const "_Assert"}, _) $ b' => b'
            | _ => cond) handle Match => cond;

        in
          Syntax.const @{syntax_const "_While_guard_inv_var"} $
            cond_guards_lst_tr' ctxt (dest_list gs) $ b' $ I $ V $
            (Syntax.const @{syntax_const "_DoPre"} $ c)
        end
    | whileAnnoG_tr' _ _ = raise Match;

  fun whileAnnoGFix_tr' ctxt [gs, cond as (Const (@{const_syntax Collect}, _) $ b), I, V, c] =
    let
      val b' =
        (case assert_tr' ctxt [b] of
          Const (@{syntax_const "_Assert"}, _) $ b' => b'
        | _ => cond) handle Match => cond;
    in
      (case maps strip_abs_vars [I, V, c] of
        [] => raise Match
      | ((x, T) :: xs) =>
          let
            val (x', I') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, strip_abs_body I);
            val (_ , V') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, strip_abs_body V);
            val (_ , c') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, strip_abs_body c);
          in
            Syntax.const @{syntax_const "_WhileFix_guard_inv_var"} $
              cond_guards_lst_tr' ctxt (dest_list gs) $ b' $ x' $ I' $ V' $
              (Syntax.const @{syntax_const "_DoPre"} $ c')
          end)
    end;
end


end;