From 5d765732c3e22558e5f1da318107e57defd11f74 Mon Sep 17 00:00:00 2001 From: amblaf Date: Mon, 7 Jun 2021 10:05:34 +1000 Subject: [PATCH] fix #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 | 2 +- c-refinement/Cogent_Corres.thy | 16 ++--- c-refinement/Type_Relation_Generation.thy | 8 ++- cogent/isa/Cogent.thy | 21 +++---- cogent/isa/CogentHelper.thy | 2 +- cogent/isa/Correspondence.thy | 46 ++++++++------- cogent/isa/Mono.thy | 4 +- cogent/isa/TypeTrackingSemantics.thy | 8 +-- cogent/isa/UpdateSemantics.thy | 72 +++++++++++++---------- cogent/isa/ValueSemantics.thy | 4 +- cogent/isa/shallow/Shallow.thy | 2 +- cogent/src/Cogent/Isabelle/Shallow.hs | 2 +- 12 files changed, 105 insertions(+), 82 deletions(-) diff --git a/c-refinement/CogentHigherOrder.thy b/c-refinement/CogentHigherOrder.thy index 5183bd6ca..6a8c128ac 100644 --- a/c-refinement/CogentHigherOrder.thy +++ b/c-refinement/CogentHigherOrder.thy @@ -89,7 +89,7 @@ fun funcall_sem :: "'f InValue env \ 'f expr \ ('f FunCa | "funcall_sem \ (Con _ tag x) = (let (calls, ptrs) = funcall_sem \ x in (calls, map ((#) (InSum tag)) ptrs))" -| "funcall_sem \ (Struct tys xs) = +| "funcall_sem \ (Struct ns tys xs) = (let (callss, ptrss) = unzip (map (funcall_sem \) xs) in (concat callss, concat (map (\(n, v). map ((#) (InRecord n)) v) (enumerate 0 ptrss))))" | "funcall_sem \ (Member x f) = diff --git a/c-refinement/Cogent_Corres.thy b/c-refinement/Cogent_Corres.thy index 06e50435d..32d5ce40c 100644 --- a/c-refinement/Cogent_Corres.thy +++ b/c-refinement/Cogent_Corres.thy @@ -491,8 +491,8 @@ qed (simp add: u_sem_all_empty) lemma corres_struct: assumes "\\ s. (\, s) \ srel \ - val_rel (URecord (zip (map (nth \) xs) (map type_repr ts))) p" -shows "corres srel (Struct ts (map Var xs)) (gets (\_. p)) \ \ \ \ \ s" + val_rel (URecord (zip (map (nth \) xs) (zip ns (map type_repr ts)))) p" +shows "corres srel (Struct ns ts (map Var xs)) (gets (\_. p)) \ \ \ \ \ 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 _ \ guard (\s. is_valid s x'); z \ gets f'; e' z od) \ \ \ \ \ s" proof - - have HELP: "\tag t b. typ ! f = (tag, t, b) \ map (type_repr \ fst \ snd) typ = map (type_repr \ fst \ 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: "\tag t b. typ ! f = (tag, t, b) \ map (\ (n,t,_). (n, type_repr t)) typ = map (\ (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 (\(n, t, b). type_repr t) typ)" + "repr = RRecord (map (\(n, t, b). (n, type_repr t)) typ)" "w13p = insert p w13" "\, \ \* fs :ur typ \r13', w13\" "\ 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'" "\, \(p \ URecord (fs[f := (\ ! e, snd (fs ! f))])) \* (fs[f := (\ ! e, snd (fs ! f))]) :ur typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)] \r1', w1'\" "distinct (map fst (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))" - "repr = RRecord (map (type_repr \ fst \ snd) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))" + "repr = RRecord (map (\ (n,t,_). (n, type_repr t)) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))" "sgl = Boxed Writable ptrl" "p \ w1'" "p \ r1'" @@ -1008,12 +1008,12 @@ proof (clarsimp simp: corres_def in_monad snd_bind snd_modify snd_state_assert, by fastforce then have "\, \(p \ URecord (fs[f := (\ ! e, snd (fs ! f))])) \ - UPtr p (RRecord (map (type_repr \ fst \ snd) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))) :u + UPtr p (RRecord (map (\ (n,t,_). (n, type_repr t)) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)]))) :u TRecord typ (Boxed Writable ptrl) \r1'', insert p w1''\" using rec_elim1_lemmas taken_field1_lemmas proof (intro u_t_p_rec_w') - show "RRecord (map (type_repr \ fst \ snd) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)])) = RRecord (map (type_repr \ fst \ snd) typ)" + show "RRecord (map (\ (n,t,_). (n, type_repr t)) (typ[f := (fst (typ ! f), fst (snd (typ ! f)), Present)])) = RRecord (map (\ (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)" diff --git a/c-refinement/Type_Relation_Generation.thy b/c-refinement/Type_Relation_Generation.thy index 4a57b4684..4ef7ae665 100644 --- a/c-refinement/Type_Relation_Generation.thy +++ b/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) diff --git a/cogent/isa/Cogent.thy b/cogent/isa/Cogent.thy index 851c2a073..300bedd87 100644 --- a/cogent/isa/Cogent.thy +++ b/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 \ type \ 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 \ 'f expr \ 'f expr | "specialise \ (Prim p es) = Prim p (map (specialise \) es)" | "specialise \ (App a b) = App (specialise \ a) (specialise \ b)" | "specialise \ (Con as t e) = Con (map (\ (c,t,b). (c, instantiate \ t, b)) as) t (specialise \ e)" -| "specialise \ (Struct ts vs) = Struct (map (instantiate \) ts) (map (specialise \) vs)" +| "specialise \ (Struct ns ts vs) = Struct ns (map (instantiate \) ts) (map (specialise \) vs)" | "specialise \ (Member v f) = Member (specialise \ v) f" | "specialise \ (Unit) = Unit" | "specialise \ (Cast t e) = Cast t (specialise \ e)" @@ -800,7 +800,7 @@ typing_var : "\ K \ \ \w singleton (length ; distinct ns ; length ns = length ts ; ts' = zip ns (zip ts (replicate (length ts) Present)) - \ \ \, K, \ \ Struct ts es : TRecord ts' Unboxed" + \ \ \, K, \ \ Struct ns ts es : TRecord ts' Unboxed" | typing_member : "\ \, K, \ \ e : TRecord ts s ; K \ TRecord ts s :\ k @@ -857,7 +857,7 @@ inductive_cases typing_caseE [elim]: "\, K, \ \ Case x t inductive_cases typing_esacE [elim]: "\, K, \ \ Esac e t : \" inductive_cases typing_castE [elim]: "\, K, \ \ Cast t e : \" inductive_cases typing_letE [elim]: "\, K, \ \ Let a b : \" -inductive_cases typing_structE [elim]: "\, K, \ \ Struct ts es : \" +inductive_cases typing_structE [elim]: "\, K, \ \ Struct ns ts es : \" inductive_cases typing_letbE [elim]: "\, K, \ \ LetBang vs a b : \" inductive_cases typing_takeE [elim]: "\, K, \ \ Take x f e : \" inductive_cases typing_putE [elim]: "\, K, \ \ Put x f e : \" @@ -876,7 +876,7 @@ inductive atom ::"'f expr \ 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 \ repr) list" | RProduct "repr" "repr" - | RRecord "repr list" + | RRecord "(name \ repr) list" | RUnit fun type_repr :: "type \ repr" where @@ -925,8 +925,8 @@ fun type_repr :: "type \ 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 (\(_,b,_). type_repr b) ts)" -| "type_repr (TRecord ts _) = RPtr (RRecord (map (\(_,b,_). type_repr b) ts))" +| "type_repr (TRecord ts Unboxed) = RRecord (map (\(n,b,_). (n, type_repr b)) ts)" +| "type_repr (TRecord ts _) = RPtr (RRecord (map (\(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 (\p1 p2. [] \ fst (snd p1) \ fst (snd p2)) as bs - \ map (type_repr \ fst \ snd) as = map (type_repr \ fst \ snd) bs" + \ map fst as = map fst bs + \ map (\ (n,t,_). (n, type_repr t)) as = map (\ (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 \ 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))" diff --git a/cogent/isa/CogentHelper.thy b/cogent/isa/CogentHelper.thy index e80ff9583..d14f4bf05 100644 --- a/cogent/isa/CogentHelper.thy +++ b/cogent/isa/CogentHelper.thy @@ -51,7 +51,7 @@ lemma typing_struct': "\ \, K, \ \* es : ts ; distinct ns ; map (fst \ snd) ts' = ts ; list_all (\p. snd (snd p) = Present) ts' - \ \ \, K, \ \ Struct ts es : TRecord ts' Unboxed" + \ \ \, K, \ \ 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': "\ \ f = (ks, t, u) diff --git a/cogent/isa/Correspondence.thy b/cogent/isa/Correspondence.thy index b3e471f76..349536831 100644 --- a/cogent/isa/Correspondence.thy +++ b/cogent/isa/Correspondence.thy @@ -38,7 +38,7 @@ inductive upd_val_rel :: "('f \ poly_type) \ bool" ("_, _ \ _ \ _ : _ \_, _\" [30,0,0,0,0,20] 80) and upd_val_rel_record :: "('f \ poly_type) \ ('f, 'au, 'l) store - \ (('f, 'au, 'l) uval \ repr) list + \ (('f, 'au, 'l) uval \ name \ repr) list \ ('f, 'av) vval list \ (name \ type \ record_state) list \ 'l set @@ -88,14 +88,14 @@ and upd_val_rel_record :: "('f \ poly_type) ; \ l = Some (URecord fs) ; s = Boxed ReadOnly ptrl ; distinct (map fst ts) - \ \ \, \ \ UPtr l (RRecord (map (type_repr \ fst \ snd) ts)) \ VRecord fs' : TRecord ts s \insert l r, {}\" + \ \ \, \ \ UPtr l (RRecord (map (\ (n,t,_). (n, type_repr t)) ts)) \ VRecord fs' : TRecord ts s \insert l r, {}\" | u_v_p_rec_w : "\ \, \ \* fs \ fs' :r ts \r, w\ ; \ l = Some (URecord fs) ; l \ (w \ r) ; s = Boxed Writable ptrl ; distinct (map fst ts) - \ \ \, \ \ UPtr l (RRecord (map (type_repr \ fst \ snd) ts)) \ VRecord fs' : TRecord ts s \r, insert l w\" + \ \ \, \ \ UPtr l (RRecord (map (\ (n,t,_). (n, type_repr t)) ts)) \ VRecord fs' : TRecord ts s \r, insert l w\" | u_v_p_abs_ro : "\ s = Boxed ReadOnly ptrl ; abs_upd_val a a' n ts s r w @@ -119,14 +119,14 @@ and upd_val_rel_record :: "('f \ poly_type) ; w \ r' = {} ; w' \ r = {} ; type_repr t = rp - \ \ \, \ \* ((x,rp) # xs) \ (x' # xs') :r ((n, t, Present) # ts) \r \ r', w \ w'\" + \ \ \, \ \* ((x,n,rp) # xs) \ (x' # xs') :r ((n, t, Present) # ts) \r \ r', w \ w'\" | u_v_r_cons2 : "\ \, \ \* xs \ xs' :r ts \r, w\ ; [] \ t wellformed ; type_repr t = rp ; upd.uval_repr x = rp ; upd.uval_repr_deep x = rp - \ \ \, \ \* ((x,rp) # xs) \ (x' # xs') :r ((n, t, Taken) # ts) \r, w\" + \ \ \, \ \* ((x,n,rp) # xs) \ (x' # xs') :r ((n, t, Taken) # ts) \r, w\" lemma upd_val_rel_to_vval_typing: shows "\, \ \ u \ v : \ \r, w\ \ val.vval_typing \ v \" @@ -293,7 +293,7 @@ lemma upd_val_rel_record: "\, \ \* vs \ vs' : ts \r, w\" "length ns = length ts" shows - "\, \ \* (zip vs (map (type_repr) ts)) \ vs' :r zip ns (zip ts (replicate (length ts) Present)) \r, w\" + "\, \ \* (zip vs (zip ns (map (type_repr) ts))) \ vs' :r zip ns (zip ts (replicate (length ts) Present)) \r, w\" using assms proof (induct arbitrary: ns rule: upd_val_rel_all.induct) qed (auto simp add: length_Suc_conv intro!: upd_val_rel_upd_val_rel_record.intros) @@ -413,8 +413,11 @@ next case u_v_p_rec_ro apply (drule upd_val_rel_to_uval_typing) apply (drule upd.uval_typing_to_wellformed(2)) apply (frule upd_val_rel_upd_val_rel_record.u_v_p_rec_ro) - apply (auto dest!: kinding_all_record' upd.bang_type_repr' - simp add: fst_apfst_compcomp snd_apsnd_compcomp map_snd3_keep) + apply (auto dest!: kinding_all_record' + simp add: map_snd3_keep) + apply(subst (asm) upd.bang_type_repr') + apply (fastforce simp add:kinding_record_def upd.bang_type_repr' split:prod.split) + apply simp done next case u_v_p_rec_w then show ?case @@ -422,8 +425,11 @@ next case u_v_p_rec_w apply (drule upd_val_rel_to_uval_typing) apply (drule upd.uval_typing_to_wellformed(2)) apply (frule upd_val_rel_upd_val_rel_record.u_v_p_rec_ro) - apply (auto dest!: kinding_all_record' upd.bang_type_repr' - simp add: fst_apfst_compcomp snd_apsnd_compcomp map_snd3_keep) + apply (auto dest!: kinding_all_record' + simp add: map_snd3_keep) + apply(subst (asm) upd.bang_type_repr') + apply (fastforce simp add:kinding_record_def upd.bang_type_repr' split:prod.split) + apply simp done next case (u_v_p_abs_ro s ptrl a a' n ts r w \ l \) @@ -1329,7 +1335,7 @@ next apply (erule conjE) apply (rule_tac x="insert l r'" in exI) apply (intro conjI, blast) - apply (rule subst[OF sym[OF subtyping_preserves_type_repr_map]], assumption) + apply (rule subst[OF sym[OF subtyping_preserves_type_repr_map]], assumption, assumption) apply (intro upd_val_rel_upd_val_rel_record.intros; blast) done next @@ -1344,7 +1350,7 @@ next apply (erule conjE) apply (rule_tac x="r'" in exI) apply (intro conjI, blast) - apply (rule subst[OF sym[OF subtyping_preserves_type_repr_map]], assumption) + apply (rule subst[OF sym[OF subtyping_preserves_type_repr_map]], assumption, assumption) apply (intro upd_val_rel_upd_val_rel_record.intros; blast) done next @@ -1422,7 +1428,7 @@ inductive_cases v_sem_caseE [elim] : " \ , \ \ Case e t inductive_cases v_sem_ifE [elim!] : " \ , \ \ If c t e \ v" inductive_cases v_sem_memberE [elim!] : " \ , \ \ Member e f \ v" inductive_cases v_sem_putE [elim!] : " \ , \ \ Put e f e' \ v" -inductive_cases v_sem_structE [elim!] : " \ , \ \ Struct fs ts \ v" +inductive_cases v_sem_structE [elim!] : " \ , \ \ Struct ns fs ts \ v" inductive_cases v_sem_tupleE [elim!] : " \ , \ \ Tuple a b \ v" inductive_cases v_sem_all_emptyE [elim!] : " \ , \ \* [] \ v" inductive_cases v_sem_all_consE [elim!] : " \ , \ \* x # xs \ v" @@ -1431,7 +1437,7 @@ lemma u_v_p_rec_w': assumes "\, \ \* fs \ fs' :r ts \r, w\" and "\ l = Some (URecord fs)" and "l \ w \ r" -and "rp = (RRecord (map (type_repr \ fst \ snd) ts)) " +and "rp = (RRecord (map (\ (n,t,_). (n, type_repr t)) ts)) " and "s = Boxed Writable ptrl" and "distinct (map fst ts)" shows "\, \ \ UPtr l rp \ VRecord fs' : TRecord ts s \ r, insert l w \" @@ -1948,8 +1954,8 @@ next case (u_sem_take \ \ \ x \'' p ra fs f e) apply (clarsimp) apply (case_tac f, simp, simp) done - have HELP2: "\ \s. ((type_repr \ fst \ snd) \ (\(n, t, y). (n, instantiate \s t, y))) - = (\(n,t,y). type_repr (instantiate \s t))" + have HELP2: "\ \s. ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, y). (n, instantiate \s t, y))) + = (\(n,t,y). (n, type_repr (instantiate \s t)))" by (force split: prod.split) from rest show ?case apply (cases e, simp_all) @@ -2096,8 +2102,8 @@ next case u_sem_put apply (clarsimp) apply (case_tac f, simp, simp) done - have HELP2: "\ \s. ((type_repr \ fst \ snd) \ (\(n, t, y). (n, instantiate \s t, y))) - = (\(n,t,y). type_repr (instantiate \s t))" + have HELP2: "\ \s. ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, y). (n, instantiate \s t, y))) + = (\(n,t,y). (n, type_repr (instantiate \s t)))" by (force split: prod.split) from rest show ?case apply (cases e, simp_all) @@ -2540,7 +2546,7 @@ next case u_sem_take and IH2 = this(5) and rest = this(1,3-4,6-) have HELP [rule_format] : - "\ tsa f t x y n. tsa ! f = (n,t,y) \ map (type_repr \ fst \ snd) tsa = map (type_repr \ fst \ snd) (tsa[f := (n, t, x)])" + "\ tsa f t x y n. tsa ! f = (n,t,y) \ map (\ (n,t,_). (n, type_repr t)) tsa = map (\ (n,t,_). (n, type_repr t)) (tsa[f := (n, t, x)])" apply (rule allI) apply (induct_tac tsa) apply (auto split: nat.split) @@ -2600,7 +2606,7 @@ next case u_sem_take_ub and IH2 = this(4) and rest = this(1,3,5-) have HELP [rule_format] : - "\ tsa f t x y n. tsa ! f = (n,t,y) \ map (type_repr \ fst \ snd) tsa = map (type_repr \ fst \ snd) (tsa[f := (n,t, x)])" + "\ tsa f t x y n. tsa ! f = (n,t,y) \ map (\ (n,t,_). (n, type_repr t)) tsa = map (\ (n,t,_). (n, type_repr t)) (tsa[f := (n,t, x)])" apply (rule allI) apply (induct_tac tsa) apply (auto split: nat.split) diff --git a/cogent/isa/Mono.thy b/cogent/isa/Mono.thy index 7bd674c4f..9c3b21afe 100644 --- a/cogent/isa/Mono.thy +++ b/cogent/isa/Mono.thy @@ -30,7 +30,7 @@ where | "rename_expr rename (Prim p es) = Prim p (map (rename_expr rename) es)" | "rename_expr rename (App a b) = App (rename_expr rename a) (rename_expr rename b)" | "rename_expr rename (Con as t e) = Con as t (rename_expr rename e)" -| "rename_expr rename (Struct ts vs) = Struct ts (map (rename_expr rename) vs)" +| "rename_expr rename (Struct ns ts vs) = Struct ns ts (map (rename_expr rename) vs)" | "rename_expr rename (Member v f) = Member (rename_expr rename v) f" | "rename_expr rename (Unit) = Unit" | "rename_expr rename (Cast t e) = Cast t (rename_expr rename e)" @@ -147,7 +147,7 @@ next apply (case_tac vval, simp_all) by (fastforce intro!: v_sem_v_sem_all.v_sem_esac) next - case (v_sem_struct \ xs vs ts \ e \ \) then show ?case + case (v_sem_struct \ xs vs ts \ ns e \ \) then show ?case by (cases e) (fastforce intro: v_sem_v_sem_all.v_sem_struct)+ next case (v_sem_if \ rb b e1 e2 v \ e \ \) diff --git a/cogent/isa/TypeTrackingSemantics.thy b/cogent/isa/TypeTrackingSemantics.thy index 7ca30d00a..807134de5 100644 --- a/cogent/isa/TypeTrackingSemantics.thy +++ b/cogent/isa/TypeTrackingSemantics.thy @@ -337,7 +337,7 @@ next "w1' = insert p w1''" "\, \'' \* fs :ur ts \r1', w1''\" "\'' p = Some (URecord fs)" - "r' = RRecord (map (type_repr \ fst \ snd) ts)" + "r' = RRecord (map (\ (n,t,_). (n, type_repr t)) ts)" "distinct (map fst ts)" "s = Boxed Writable ptrl" "p \ w1''" @@ -388,9 +388,9 @@ next proof (simp only: snd_t\4_is append_Cons append.left_neutral, intro matches_ptrs_some[OF _ matches_ptrs_some]) have "\, \'' \* fs :ur ts[f := (n, t, taken)] \r1a, w1a\" by (simp add: ut_fs_taken_f Taken) - moreover have "r' = RRecord (map (type_repr \ fst \ snd) (ts[f := (n, t, taken)]))" - using Taken type_repr_uval_repr uptr_p_elim_lemmas ut_fs_taken_f - by (metis (full_types)) + moreover have "r' = RRecord (map (\ (n,t,_). (n, type_repr t)) (ts[f := (n, t, taken)]))" + using Taken type_repr_uval_repr uptr_p_elim_lemmas ut_fs_taken_f + by metis ultimately show "\, \'' \ UPtr p r' :u TRecord (ts[f := (n, t, taken)]) s \r1a, insert p w1a\" using uptr_p_elim_lemmas ut_fs_taken_f r1'_is w1''_is by (simp, intro u_t_p_rec_w'; diff --git a/cogent/isa/UpdateSemantics.thy b/cogent/isa/UpdateSemantics.thy index f9ba69cb1..837af14bf 100644 --- a/cogent/isa/UpdateSemantics.thy +++ b/cogent/isa/UpdateSemantics.thy @@ -17,7 +17,7 @@ begin datatype ('f, 'a, 'l) uval = UPrim lit | UProduct "('f,'a,'l) uval" "('f,'a,'l) uval" | USum name "('f,'a,'l) uval" "(name \ repr) list" - | URecord "(('f,'a,'l) uval \ repr) list" + | URecord "(('f,'a,'l) uval \ name \ repr) list" | UAbstract "'a" | UFunction "'f expr" "type list" | UAFunction "'f" "type list" @@ -121,7 +121,7 @@ where \ \ \ , \ \ (\, If x t e) \! st" | u_sem_struct : "\ \ , \ \* (\, xs) \! (\', vs) - \ \ \ , \ \ (\, Struct ts xs) \! (\', URecord (zip vs (map type_repr ts)))" + \ \ \ , \ \ (\, Struct ns ts xs) \! (\', URecord (zip vs (zip ns (map type_repr ts))))" | u_sem_take : "\ \ , \ \ (\, x) \! (\', UPtr p r) ; \' p = Some (URecord fs) @@ -188,7 +188,7 @@ fun uval_repr_deep :: "('f, 'a, 'l) uval \ repr" where "uval_repr_deep (UPrim lit) = RPrim (lit_type lit)" | "uval_repr_deep (UProduct a b) = RProduct (uval_repr_deep a) (uval_repr_deep b)" | "uval_repr_deep (USum a b reprs) = RSum reprs" -| "uval_repr_deep (URecord fs) = RRecord (map uval_repr_deep (map fst fs))" +| "uval_repr_deep (URecord fs) = RRecord (map (\ (f,n,_). (n, uval_repr_deep f)) fs) " | "uval_repr_deep (UAbstract a) = (let (x,y) = abs_repr a in RCon x y)" | "uval_repr_deep (UFunction _ _) = RFun" | "uval_repr_deep (UAFunction _ _) = RFun" @@ -204,7 +204,7 @@ inductive uval_typing :: "('f \ poly_type) \ bool" ("_, _ \ _ :u _ \_, _\" [30,0,0,0,20] 80) and uval_typing_record :: "('f \ poly_type) \ ('f, 'a, 'l) store - \ (('f, 'a, 'l) uval \ repr) list + \ (('f, 'a, 'l) uval \ name \ repr) list \ (name \ type \ record_state) list \ 'l set \ 'l set @@ -252,13 +252,13 @@ and uval_typing_record :: "('f \ poly_type) | u_t_p_rec_ro : "\ \, \ \* fs :ur ts \r, {}\ ; \ l = Some (URecord fs) ; distinct (map fst ts) - \ \ \, \ \ UPtr l (RRecord (map (type_repr \ fst \ snd) ts)) :u TRecord ts (Boxed ReadOnly ptrl) \insert l r, {}\" + \ \ \, \ \ UPtr l (RRecord (map (\ (n,t,_). (n, type_repr t)) ts)) :u TRecord ts (Boxed ReadOnly ptrl) \insert l r, {}\" | u_t_p_rec_w : "\ \, \ \* fs :ur ts \r, w\ ; \ l = Some (URecord fs) ; l \ (w \ r) ; distinct (map fst ts) - \ \ \, \ \ UPtr l (RRecord (map (type_repr \ fst \ snd) ts)) :u TRecord ts (Boxed Writable ptrl) \r, insert l w\" + \ \ \, \ \ UPtr l (RRecord (map (\ (n,t,_). (n, type_repr t)) ts)) :u TRecord ts (Boxed Writable ptrl) \r, insert l w\" | u_t_p_abs_ro : "\ s = Boxed ReadOnly ptrl ; abs_typing a n ts s r {} @@ -280,14 +280,14 @@ and uval_typing_record :: "('f \ poly_type) ; w \ r' = {} ; w' \ r = {} ; type_repr t = rp - \ \ \, \ \* ((x,rp) # xs) :ur ((n, t, Present) # ts) \r \ r', w \ w'\" + \ \ \, \ \* ((x,n,rp) # xs) :ur ((n, t, Present) # ts) \r \ r', w \ w'\" | u_t_r_cons2 : "\ \, \ \* xs :ur ts \r, w\ ; [] \ t wellformed ; type_repr t = rp ; uval_repr x = rp ; uval_repr_deep x = rp - \ \ \, \ \* ((x,rp) # xs) :ur ((n, t, Taken) # ts) \r, w\" + \ \ \, \ \* ((x,n,rp) # xs) :ur ((n, t, Taken) # ts) \r, w\" lemma u_t_prim' : "\ = lit_type l \ \, \ \ UPrim l :u TPrim \ \{}, {}\" by (simp add: u_t_prim) @@ -378,7 +378,7 @@ lemma uval_typing_all_record: "\, \ \* vs :u ts \r, w\" "length ns = length ts" shows - "\, \ \* (zip vs (map (type_repr) ts)) :ur zip ns (zip ts (replicate (length ts) Present)) \r, w\" + "\, \ \* zip vs (zip ns (map (type_repr) ts)) :ur zip ns (zip ts (replicate (length ts) Present)) \r, w\" using assms proof (induct arbitrary: ns rule: uval_typing_all.induct) qed (auto intro!: uval_typing_uval_typing_record.intros simp add: length_Suc_conv) @@ -536,10 +536,17 @@ lemma list_all2_bang_type_helper: lemma bang_type_repr': assumes "[] \* ts :\r k" -shows "(map (type_repr \ fst \ snd \ apsnd (apfst bang)) ts) = (map (type_repr \ fst \ snd) ts)" +shows "(map ((\ (n,t,_). (n, type_repr t)) \ apsnd (apfst bang)) ts) = (map (\ (n,t,_). (n, type_repr t)) ts)" using assms by (fastforce dest: bang_type_repr) +lemma bang_type_repr'' : + assumes "[] \* map (fst \ snd) ts wellformed" + shows "(map ((\ (n,t,_). (n, type_repr t)) \ apsnd (apfst bang)) ts) = (map (\ (n,t,_). (n, type_repr t)) ts)" + using assms + by (fastforce dest: bang_type_repr) + + lemma uval_typing_bang: shows "\, \ \ v :u \ \r, w\ \ \, \ \ v :u bang \ \r \ w, {}\" and "\, \ \* vs :ur \s \r, w\ \ \, \ \* vs :ur (map (apsnd (apfst bang)) \s) \r \ w, {}\" @@ -556,17 +563,20 @@ next by (force intro: uval_typing_uval_typing_record.intros bang_wellformed abs_typing_bang[where s = Unboxed, simplified]) next case (u_t_p_rec_ro \ \ fs ts r l ptrl) - moreover have "\, \ \ UPtr l (RRecord (map (type_repr \ fst \ snd \ apsnd (apfst bang)) ts)) :u TRecord (map (apsnd (apfst bang)) ts) (Boxed ReadOnly ptrl) \insert l r, {}\" + moreover have "\, \ \ UPtr l (RRecord (map ((\ (n,t,_). (n, type_repr t)) \ apsnd (apfst bang)) ts)) :u TRecord (map (apsnd (apfst bang)) ts) (Boxed ReadOnly ptrl) \insert l r, {}\" using u_t_p_rec_ro by (fastforce dest: uval_typing_to_wellformed(2) uval_typing_uval_typing_record.u_t_p_rec_ro) ultimately show ?case - by (force dest: uval_typing_to_wellformed(2) simp add: fst_apfst_compcomp snd_apsnd_compcomp map_snd3_keep) + apply(subst (asm) bang_type_repr'') + using uval_typing_to_wellformed(2) + apply blast + by (simp add: map_snd3_keep) next case (u_t_p_rec_w \ \ fs ts r w l ptrl) - moreover have "\, \ \ UPtr l (RRecord (map (type_repr \ fst \ snd \ apsnd (apfst bang)) ts)) :u TRecord (map (apsnd (apfst bang)) ts) (Boxed ReadOnly ptrl) \insert l (r \ w), {}\" + moreover have "\, \ \ UPtr l (RRecord (map ((\ (n,t,_). (n, type_repr t)) \ apsnd (apfst bang)) ts)) :u TRecord (map (apsnd (apfst bang)) ts) (Boxed ReadOnly ptrl) \insert l (r \ w), {}\" using u_t_p_rec_w uval_typing_uval_typing_record.u_t_p_rec_ro by fastforce ultimately show ?case - by (auto dest!: uval_typing_to_wellformed(2) simp add: fst_apfst_compcomp snd_apsnd_compcomp map_snd3_keep) + by (auto dest!: uval_typing_to_wellformed(2) simp add: bang_type_repr'' fst_apfst_compcomp snd_apsnd_compcomp map_snd3_keep) next case (u_t_p_abs_ro s ptrl a n ts r \ l \) then have "\, \ \ UPtr l (RCon n (map type_repr (map bang ts))) :u TCon n (map bang ts) (Boxed ReadOnly ptrl) \insert l r, {}\" @@ -1338,13 +1348,13 @@ using assms(2,1) by ( induct "map snd tsa" "map snd rs" lemma type_repr_uval_repr: shows"\, \ \ v :u t \r, w\ \ uval_repr v = type_repr t" -and "\, \ \* fs :ur ts \r, w\ \ map snd fs = map (type_repr \ fst \ snd) ts" +and "\, \ \* fs :ur ts \r, w\ \ map snd fs = map (\ (n,t,_). (n, type_repr t)) ts" by (induct rule: uval_typing_uval_typing_record.inducts, (force dest: abs_typing_repr intro: list_all2_helper2 [symmetric])+) lemma type_repr_uval_repr_deep: shows"\, \ \ v :u t \r, w\ \ uval_repr_deep v = type_repr t" -and "\, \ \* fs :ur ts \r, w\ \ map uval_repr_deep (map fst fs) = map (type_repr \ fst \ snd) ts" +and "\, \ \* fs :ur ts \r, w\ \ map (\ (u,n,_). (n, uval_repr_deep u)) fs = map (\ (n,t,_). (n, type_repr t)) ts" by (induct rule: uval_typing_uval_typing_record.inducts, (force dest: abs_typing_repr intro: list_all2_helper2 [symmetric])+) @@ -1451,7 +1461,7 @@ proof (induct fs arbitrary: f r'a w'a ts) "\, \ \* fs'[fa := (e', snd (fs' ! fa))] :ur ts'[fa := (n, t, Present)] \r''a \ r'b, w' \ w'b\" using u_t_r_cons1 Cons Suc by (clarsimp simp add: w'b_empty Int_Un_distrib2, meson) - then have "\, \ \* (x, rp) # fs'[fa := (e', snd (fs' ! fa))] :ur (n', t', Present) # ts'[fa := (n, t, Present)] \r \ (r''a \ r'b), w \ (w' \ w'b)\" + then have "\, \ \* (x, n', rp) # fs'[fa := (e', snd (fs' ! fa))] :ur (n', t', Present) # ts'[fa := (n, t, Present)] \r \ (r''a \ r'b), w \ (w' \ w'b)\" using u_t_r_cons1 Cons.prems by (auto intro!: uval_typing_uval_typing_record.u_t_r_cons1 simp add: Int_Un_distrib Int_Un_distrib2) then show ?thesis @@ -1616,8 +1626,8 @@ next obtain r' where fields: "\, \ \* fs :ur ts' \r', {}\" "r' \ r" using elims subty_trecord subtyping_simps(6) u_t_p_rec_ro by meson - have repr_same: "map (type_repr \ fst \ snd) ts = map (type_repr \ fst \ snd) ts'" - using elims(3) + have repr_same: "map (\ (n,t,_). (n, type_repr t)) ts = map (\ (n,t,_). (n, type_repr t)) ts'" + using elims(3,2) by (induct rule: list_all2_induct; auto simp add: subtyping_preserves_type_repr) show ?case @@ -1637,8 +1647,8 @@ next obtain r' where fields: "\, \ \* fs :ur ts' \r', w\" "r' \ r" using elims subty_trecord subtyping_simps(6) u_t_p_rec_w by meson - have repr_same: "map (type_repr \ fst \ snd) ts = map (type_repr \ fst \ snd) ts'" - using elims(3) + have repr_same: "map (\ (n,t,_). (n, type_repr t)) ts = map (\ (n,t,_). (n, type_repr t)) ts'" + using elims(3,2) by (induct rule: list_all2_induct; auto simp add: subtyping_preserves_type_repr) show ?case @@ -1687,7 +1697,7 @@ next moreover have w_empty: "w = {}" using discardable_not_writable field_is' u_t_r_cons1 by (metis calculation record_state.distinct(1) singletonI) - moreover have "\, \ \* (x, rp) # xs :ur (n, t2, Taken) # ts2' \rts2', w'\" + moreover have "\, \ \* (x, n, rp) # xs :ur (n, t2, Taken) # ts2' \rts2', w'\" using field_rest repr_same t2_wf by (auto intro: uval_typing_uval_typing_record.u_t_r_cons2) ultimately show ?thesis @@ -1777,7 +1787,7 @@ lemma u_t_p_rec_w': assumes "\, \ \* fs :ur ts \r, w\" and "\ l = Some (URecord fs)" and "l \ w \ r" - and "rp = (RRecord (map (type_repr \ fst \ snd) ts)) " + and "rp = (RRecord (map (\ (n,t,_). (n, type_repr t)) ts)) " and "distinct (map fst ts)" shows "\, \ \ UPtr l rp :u TRecord ts (Boxed Writable ptrl) \ r, insert l w \" using assms @@ -2381,7 +2391,7 @@ next "\, \'' \* fs :ur map (\(n, t, y). (n, instantiate \s t, y)) ts \r1', w1'\" "\'' pa = Some (URecord fs)" "distinct (map fst ts)" - "ra = RRecord (map (type_repr \ fst \ snd \ (\(n, t, b). (n, instantiate \s t, b))) ts)" + "ra = RRecord (map ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, b). (n, instantiate \s t, b))) ts)" "s = Boxed Writable ptrl" "pa \ w1'" "pa \ r1'" @@ -2418,11 +2428,11 @@ next using matches_ptrs_frame ptrs_split_lemmas IH1_lemmas by blast - have "map ((type_repr \ fst \ snd) \ (\(n, t, y). (n, instantiate \s t, y))) ts ! f' = type_repr (instantiate \s t)" + have "map ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, y). (n, instantiate \s t, y))) ts ! f' = (n, type_repr (instantiate \s t))" by (simp add: typing_e_elim_lemmas(4) typing_e_elim_lemmas(5)) then have type_repr_inst_ts_taken_same: - "map ((type_repr \ fst \ snd) \ (\(n, t, y). (n, instantiate \s t, y))) (ts[f' := (n, t, taken)]) - = map ((type_repr \ fst \ snd) \ (\(n, t, y). (n, instantiate \s t, y))) ts" + "map ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, y). (n, instantiate \s t, y))) (ts[f' := (n, t, taken)]) + = map ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, y). (n, instantiate \s t, y))) ts" by (simp add: map_update list_helper) show ?thesis @@ -2436,7 +2446,7 @@ next \r1'' \ (r1''' \ r2), w1'' \ (insert pa w1''' \ w2)\" using utype_record_take_lemmas u_sem_take.hyps(3) \''_matches2 proof (intro matches_ptrs_some[OF _ matches_ptrs_some[OF u_t_p_rec_w']]) - show "ra = RRecord (map (type_repr \ fst \ snd) ((map (\(n, t, y). (n, instantiate \s t, y)) ts)[f' := (n, instantiate \s t, Taken)]))" + show "ra = RRecord (map (\ (n,t,_). (n, type_repr t)) ((map (\(n, t, y). (n, instantiate \s t, y)) ts)[f' := (n, instantiate \s t, Taken)]))" using type_repr_inst_ts_taken_same IH1_uptr_elim_lemmas by (simp add: map_update) next @@ -2608,8 +2618,8 @@ next case u_sem_put apply (clarsimp) apply (case_tac f, simp, simp) done - have HELP2: "\ \s. (type_repr \ fst \ snd \ (\(n, t, y). (n, instantiate \s t, y))) - = (\(n, t, y). type_repr (instantiate \s t))" + have HELP2: "\ \s. ((\ (n,t,_). (n, type_repr t)) \ (\(n, t, y). (n, instantiate \s t, y))) + = (\(n, t, y). (n, type_repr (instantiate \s t)))" by (force split: prod.split) from rest show ?case apply (cases e, simp_all) @@ -2783,7 +2793,7 @@ lemma type_repr_heap: shows "\ \, \ \ v :u t \r, w\; \, \ \ v :u t' \r', w'\ \ \ type_repr t = type_repr t'" and "\ \, \ \* fs :ur ts \r, w\ ; \, \ \* fs :ur ts' \r', w'\ - \ \ (map (type_repr \ fst \ snd) ts) = (map (type_repr \ fst \ snd) ts')" + \ \ (map (\ (n,t,_). (n, type_repr t)) ts) = (map (\ (n,t,_). (n, type_repr t)) ts')" by (auto dest!: type_repr_uval_repr) diff --git a/cogent/isa/ValueSemantics.thy b/cogent/isa/ValueSemantics.thy index c3fa34b2a..0ff2e4a36 100644 --- a/cogent/isa/ValueSemantics.thy +++ b/cogent/isa/ValueSemantics.thy @@ -117,7 +117,7 @@ where \ \ \ , \ \ If x t e \ r" | v_sem_struct : "\ \ , \ \* xs \ vs - \ \ \ , \ \ Struct ts xs \ VRecord vs" + \ \ \ , \ \ Struct ns ts xs \ VRecord vs" | v_sem_take : "\ \ , \ \ x \ VRecord fs ; \ , (fs ! f # VRecord fs # \) \ e \ e' @@ -1145,7 +1145,7 @@ function monoexpr :: "'f expr \ ('f \ type list) expr" where | "monoexpr (Prim p es) = Prim p (map (monoexpr) es)" | "monoexpr (App a b) = App (monoexpr a) (monoexpr b)" | "monoexpr (Con as t e) = Con as t (monoexpr e)" -| "monoexpr (Struct ts vs) = Struct ts (map (monoexpr) vs)" +| "monoexpr (Struct ns ts vs) = Struct ns ts (map (monoexpr) vs)" | "monoexpr (Member v f) = Member (monoexpr v) f" | "monoexpr (Unit) = Unit" | "monoexpr (Cast t e) = Cast t (monoexpr e)" diff --git a/cogent/isa/shallow/Shallow.thy b/cogent/isa/shallow/Shallow.thy index 0e11c4a9d..463a83cb5 100644 --- a/cogent/isa/shallow/Shallow.thy +++ b/cogent/isa/shallow/Shallow.thy @@ -32,7 +32,7 @@ inductive_cases v_sem_splitE: "\ , \ \ Split x e \ e inductive_cases v_sem_takeE: "\ , \ \ Take x f e \ e'" inductive_cases v_sem_putE: "\ , \ \ Put x f e \ e'" inductive_cases v_sem_castE: "\ , \ \ Cast \ e \ e'" -inductive_cases v_sem_structE: "\ , \ \ Struct ts xs \ e'" +inductive_cases v_sem_structE: "\ , \ \ Struct ns ts xs \ e'" inductive_cases v_sem_AppE: "\ , \ \ App f v \ e'" inductive_cases v_sem_allE: "\ , \ \* es \ es'" inductive_cases v_sem_all_NilE: "\ , \ \* [] \ es'" diff --git a/cogent/src/Cogent/Isabelle/Shallow.hs b/cogent/src/Cogent/Isabelle/Shallow.hs index 067d13bdf..b391ee81c 100644 --- a/cogent/src/Cogent/Isabelle/Shallow.hs +++ b/cogent/src/Cogent/Isabelle/Shallow.hs @@ -1019,7 +1019,7 @@ scorresStructLemma name fields = let assums = [ "scorres " ++ x ++ " " ++ y ++ " \\ \\" | (x, y) <- P.zip (varNames "s") (varNames "d") ] concl = "scorres (" ++ name ++ ".make " ++ unwords (varNames "s") ++ ") " ++ - "(Struct ts [" ++ intercalate ", " (varNames "d") ++ "]) \\ \\" + "(Struct ns ts [" ++ intercalate ", " (varNames "d") ++ "]) \\ \\" prop = "\\" ++ intercalate " " all_names ++ ".\n" ++ intercalate " \\\n" (assums ++ [concl]) method = Method "clarsimp" ["simp:", "scorres_def", "valRel_" ++ name, name ++ ".defs", "elim!:", "v_sem_elims"]