fix au-ts#377: field names in uval (and expr, repr)

Representations of types should be in one-to-one correspondance with
C types for the put lemmas to be right. Thus they should contain
the field names for records.

c-refinement/CogentHigherOrder.thy

@@ -89,7 +89,7 @@ fun funcall_sem :: "'f InValue env \<Rightarrow> 'f expr \<Rightarrow> ('f FunCa
 | "funcall_sem \<gamma> (Con _ tag x) =
      (let (calls, ptrs) = funcall_sem \<gamma> x
       in (calls, map ((#) (InSum tag)) ptrs))"
-| "funcall_sem \<gamma> (Struct tys xs) =
+| "funcall_sem \<gamma> (Struct ns tys xs) =
      (let (callss, ptrss) = unzip (map (funcall_sem \<gamma>) xs)
       in (concat callss, concat (map (\<lambda>(n, v). map ((#) (InRecord n)) v) (enumerate 0 ptrss))))"
 | "funcall_sem \<gamma> (Member x f) =

c-refinement/Cogent_Corres.thy

@@ -491,8 +491,8 @@ qed (simp add: u_sem_all_empty)
 lemma corres_struct:
 assumes
  "\<And>\<sigma> s. (\<sigma>, s) \<in> srel \<Longrightarrow>
-  val_rel (URecord (zip (map (nth \<gamma>) xs) (map type_repr ts))) p"
-shows "corres srel (Struct ts (map Var xs)) (gets (\<lambda>_. p)) \<xi> \<gamma> \<Xi> \<Gamma> \<sigma> s"
+  val_rel (URecord (zip (map (nth \<gamma>) xs) (zip ns (map type_repr ts)))) p"
+shows "corres srel (Struct ns ts (map Var xs)) (gets (\<lambda>_. p)) \<xi> \<gamma> \<Xi> \<Gamma> \<sigma> s"
   by (fastforce intro: u_sem_struct u_sem_all_var simp: assms corres_def snd_return in_return)
 
 lemma corres_con:
@@ -701,8 +701,8 @@ lemma corres_take_boxed':
   (do _ \<leftarrow> guard (\<lambda>s. is_valid s x'); z \<leftarrow> gets f'; e' z od)
   \<xi> \<gamma> \<Xi> \<Gamma> \<sigma> s"
 proof -
-  have HELP: "\<And>tag t b. typ ! f = (tag, t, b) \<Longrightarrow> map (type_repr \<circ> fst \<circ> snd) typ = map (type_repr \<circ> fst \<circ> snd) (typ[f := (tag, t, Present)])"
-    by (simp add: map_update, metis (mono_tags, lifting) comp_def list_update_id map_update prod_injects(1))
+  have HELP: "\<And>tag t b. typ ! f = (tag, t, b) \<Longrightarrow> map (\<lambda> (n,t,_). (n, type_repr t)) typ = map (\<lambda> (n,t,_). (n, type_repr t)) (typ[f := (tag, t, Present)])"
+    by (simp add: map_update, metis (mono_tags, lifting)  old.prod.case list_update_id map_update prod_injects(1))
   show ?thesis
     apply (clarsimp simp: corres_def in_monad snd_bind snd_gets snd_state_assert)
     apply (rename_tac r w)
@@ -965,7 +965,7 @@ proof (clarsimp simp: corres_def in_monad snd_bind snd_modify snd_state_assert,
 
   obtain fs w13
     where uval_typing1_elim_lemmas:
-      "repr = RRecord (map (\<lambda>(n, t, b). type_repr t) typ)"
+      "repr = RRecord (map (\<lambda>(n, t, b). (n, type_repr t)) typ)"
       "w13p = insert p w13"
       "\<Xi>, \<sigma> \<turnstile>* fs :ur typ \<langle>r13', w13\<rangle>"
       "\<sigma> p = Some (URecord fs)"
@@ -991,7 +991,7 @@ proof (clarsimp simp: corres_def in_monad snd_bind snd_modify snd_state_assert,
         "w1p' = insert p w1'"
         "\<Xi>, \<sigma>(p \<mapsto> URecord (fs[f := (\<gamma> ! e, snd (fs ! f))])) \<turnstile>* (fs[f := (\<gamma> ! e, snd (fs ! f))]) :ur typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)] \<langle>r1', w1'\<rangle>"
         "distinct (map fst (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))"
-        "repr = RRecord (map (type_repr \<circ> fst \<circ> snd) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))"
+        "repr = RRecord (map (\<lambda> (n,t,_). (n, type_repr t)) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))"
         "sgl = Boxed Writable ptrl"
         "p \<notin> w1'"
         "p \<notin> r1'"
@@ -1008,12 +1008,12 @@ proof (clarsimp simp: corres_def in_monad snd_bind snd_modify snd_state_assert,
     by fastforce
 
   then have "\<Xi>, \<sigma>(p \<mapsto> URecord (fs[f := (\<gamma> ! e, snd (fs ! f))])) \<turnstile>
-              UPtr p (RRecord (map (type_repr \<circ> fst \<circ> snd) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))) :u
+              UPtr p (RRecord (map (\<lambda> (n,t,_). (n, type_repr t)) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))) :u
               TRecord typ (Boxed Writable ptrl)
             \<langle>r1'', insert p w1''\<rangle>"
     using rec_elim1_lemmas taken_field1_lemmas
   proof (intro u_t_p_rec_w')
-    show "RRecord (map (type_repr \<circ> fst \<circ> snd) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)])) = RRecord (map (type_repr \<circ> fst \<circ> snd) typ)"
+    show "RRecord (map (\<lambda> (n,t,_). (n, type_repr t)) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)])) = RRecord (map (\<lambda> (n,t,_). (n, type_repr t)) typ)"
       by (clarsimp, metis rec_elim1_lemmas(2) taken_field1_lemmas(3) type_repr_uval_repr(2))
   next
     show "distinct (map fst typ)"

c-refinement/Type_Relation_Generation.thy

@@ -25,12 +25,18 @@ fun mk_rhs_of_type_rel_rec _ (field_info:HeapLiftBase.field_info list) =
  * We assume that there are (length field_info) bound variables
  * corresponding to the type repr for each field. *)
  let
+  val _ = @{print} field_info
   val num_fields = List.length field_info;
 
   (* mk_hd_conjct makes e.g. @{term "ty = TRecord [(''a'', a), (''b'', b)]"} in the body.*)
   val mk_hd_conjct =
    let
-    val ml_list_for_TRecord = map_index (fn (n, _) => Bound (num_fields - n - 1)) field_info;
+    fun make_name s = if String.isSuffix "_C" s then 
+                           (* remove the _C suffix *)
+                           String.substring (s, 0, String.size s - 2) 
+                      else error ("mk_rhs_of_type_rel_rec: not a C field " ^ s)
+    val ml_list_for_TRecord = map_index (fn (n, i ) =>
+     encode_isa_pair (HOLogic.mk_string (# name i |> make_name), Bound (num_fields - n - 1))) field_info;
     val RRecord = Const (@{const_name RRecord}, dummyT) $ mk_isa_list ml_list_for_TRecord
    in
     HOLogic.mk_eq (Free ("ty", dummyT), RRecord)

cogent/isa/Cogent.thy

@@ -319,7 +319,7 @@ datatype 'f expr = Var index
                  | Prim prim_op "'f expr list"
                  | App "'f expr" "'f expr"
                  | Con "(name \<times> type \<times> variant_state) list" name "'f expr"
-                 | Struct "type list" "'f expr list"
+                 | Struct "name list" "type list" "'f expr list"
                  | Member "'f expr" field
                  | Unit
                  | Lit lit
@@ -473,7 +473,7 @@ fun specialise :: "type substitution \<Rightarrow> 'f expr \<Rightarrow> 'f expr
 | "specialise \<delta> (Prim p es)       = Prim p (map (specialise \<delta>) es)"
 | "specialise \<delta> (App a b)         = App (specialise \<delta> a) (specialise \<delta> b)"
 | "specialise \<delta> (Con as t e)      = Con (map (\<lambda> (c,t,b). (c, instantiate \<delta> t, b)) as) t (specialise \<delta> e)"
-| "specialise \<delta> (Struct ts vs)    = Struct (map (instantiate \<delta>) ts) (map (specialise \<delta>) vs)"
+| "specialise \<delta> (Struct ns ts vs)    = Struct ns (map (instantiate \<delta>) ts) (map (specialise \<delta>) vs)"
 | "specialise \<delta> (Member v f)      = Member (specialise \<delta> v) f"
 | "specialise \<delta> (Unit)            = Unit"
 | "specialise \<delta> (Cast t e)        = Cast t (specialise \<delta> e)"
@@ -800,7 +800,7 @@ typing_var    : "\<lbrakk> K \<turnstile> \<Gamma> \<leadsto>w singleton (length
                    ; distinct ns
                    ; length ns = length ts
                    ; ts' = zip ns (zip ts (replicate (length ts) Present))
-                   \<rbrakk> \<Longrightarrow> \<Xi>, K, \<Gamma> \<turnstile> Struct ts es : TRecord ts' Unboxed"
+                   \<rbrakk> \<Longrightarrow> \<Xi>, K, \<Gamma> \<turnstile> Struct ns ts es : TRecord ts' Unboxed"
 
 | typing_member : "\<lbrakk> \<Xi>, K, \<Gamma> \<turnstile> e : TRecord ts s
                    ; K \<turnstile> TRecord ts s :\<kappa> k
@@ -857,7 +857,7 @@ inductive_cases typing_caseE   [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Case x t
 inductive_cases typing_esacE   [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Esac e t : \<tau>"
 inductive_cases typing_castE   [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Cast t e : \<tau>"
 inductive_cases typing_letE    [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Let a b : \<tau>"
-inductive_cases typing_structE [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Struct ts es : \<tau>"
+inductive_cases typing_structE [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Struct ns ts es : \<tau>"
 inductive_cases typing_letbE   [elim]: "\<Xi>, K, \<Gamma> \<turnstile> LetBang vs a b : \<tau>"
 inductive_cases typing_takeE   [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Take x f e : \<tau>"
 inductive_cases typing_putE    [elim]: "\<Xi>, K, \<Gamma> \<turnstile> Put x f e : \<tau>"
@@ -876,7 +876,7 @@ inductive atom ::"'f expr \<Rightarrow> bool" where
 | "atom (AFun f ts)"
 | "atom (Prim p (map Var is))"
 | "atom (Con ts n (Var x))"
-| "atom (Struct ts (map Var is))"
+| "atom (Struct ns ts (map Var is))"
 | "atom (Cast t (Var x))"
 | "atom (Member (Var x) f)"
 | "atom Unit"
@@ -915,7 +915,7 @@ datatype repr = RPtr repr
               | RPrim prim_type
               | RSum "(name \<times> repr) list"
               | RProduct "repr" "repr"
-              | RRecord "repr list"
+              | RRecord "(name \<times> repr) list"
               | RUnit
 
 fun type_repr :: "type \<Rightarrow> repr" where
@@ -925,8 +925,8 @@ fun type_repr :: "type \<Rightarrow> repr" where
 | "type_repr (TProduct a b)       = RProduct (type_repr a) (type_repr b)"
 | "type_repr (TCon n ts Unboxed)  = RCon n (map type_repr ts)"
 | "type_repr (TCon n ts _)        = RPtr (RCon n (map type_repr ts))"
-| "type_repr (TRecord ts Unboxed) = RRecord (map (\<lambda>(_,b,_). type_repr b) ts)"
-| "type_repr (TRecord ts _)       = RPtr (RRecord (map (\<lambda>(_,b,_). type_repr b) ts))"
+| "type_repr (TRecord ts Unboxed) = RRecord (map (\<lambda>(n,b,_). (n, type_repr b)) ts)"
+| "type_repr (TRecord ts _)       = RPtr (RRecord (map (\<lambda>(n,b,_). (n, type_repr b)) ts))"
 | "type_repr (TUnit)              = RUnit"
 
 
@@ -1553,7 +1553,8 @@ qed auto
 
 lemma subtyping_preserves_type_repr_map:
   "list_all2 (\<lambda>p1 p2. [] \<turnstile> fst (snd p1) \<sqsubseteq> fst (snd p2)) as bs
-  \<Longrightarrow> map (type_repr \<circ> fst \<circ> snd) as = map (type_repr \<circ> fst \<circ> snd) bs"
+  \<Longrightarrow> map fst as = map fst bs
+  \<Longrightarrow> map (\<lambda> (n,t,_). (n, type_repr t)) as = map (\<lambda> (n,t,_). (n, type_repr t)) bs"
   by (induct rule: list_all2_induct, auto simp add: subtyping_preserves_type_repr)
 
 
@@ -2217,7 +2218,7 @@ fun expr_size :: "'f expr \<Rightarrow> nat" where
 | "expr_size (Prim p as) = Suc (sum_list (map expr_size as))"
 | "expr_size (Var v) = 0"
 | "expr_size (AFun v va) = 0"
-| "expr_size (Struct v va) = Suc (sum_list (map expr_size va))"
+| "expr_size (Struct ns v va) = Suc (sum_list (map expr_size va))"
 | "expr_size (Lit v) = 0"
 | "expr_size (SLit s) = 0"
 | "expr_size (Tuple v va) = Suc ((expr_size v) + (expr_size va))"

cogent/isa/CogentHelper.thy

@@ -51,7 +51,7 @@ lemma typing_struct': "\<lbrakk> \<Xi>, K, \<Gamma> \<turnstile>* es : ts
                        ; distinct ns
                        ; map (fst \<circ> snd) ts' = ts
                        ; list_all (\<lambda>p. snd (snd p) = Present) ts'
-                       \<rbrakk> \<Longrightarrow> \<Xi>, K, \<Gamma> \<turnstile> Struct ts es : TRecord ts' Unboxed"
+                       \<rbrakk> \<Longrightarrow> \<Xi>, K, \<Gamma> \<turnstile> Struct ns ts es : TRecord ts' Unboxed"
   by (force intro: typing_struct simp add: zip_eq_conv_sym replicate_eq_map_conv_nth list_all_length)
 
 lemma typing_afun': "\<lbrakk> \<Xi> f = (ks, t, u)