# HG changeset patch # User wenzelm # Date 1266325719 -3600 # Node ID f132a4fd8679f7ff303894231186c0978f2c3b58 # Parent 8b8302da3a550912999061fce6312b896f7f4c35 moved generic update_name to Pure syntax -- not specific to HOL/record; diff -r 8b8302da3a55 -r f132a4fd8679 src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Tue Feb 16 13:35:42 2010 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Tue Feb 16 14:08:39 2010 +0100 @@ -94,17 +94,6 @@ annquote_tr' (Syntax.const name) (r :: t :: ts) | annbexp_tr' _ _ = raise Match; - fun upd_tr' (x_upd, T) = - (case try (unsuffix Record.updateN) x_upd of - SOME x => (x, if T = dummyT then T else Term.domain_type T) - | NONE => raise Match); - - fun update_name_tr' (Free x) = Free (upd_tr' x) - | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) = - c $ Free (upd_tr' x) - | update_name_tr' (Const x) = Const (upd_tr' x) - | update_name_tr' _ = raise Match; - fun K_tr' (Abs (_, _, t)) = if null (loose_bnos t) then t else raise Match | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = @@ -112,12 +101,12 @@ | K_tr' _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f) + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) (Abs (x, dummyT, K_tr' k) :: ts) | assign_tr' _ = raise Match; fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ update_name_tr' f) + quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f) (Abs (x, dummyT, K_tr' k) :: ts) | annassign_tr' _ = raise Match; diff -r 8b8302da3a55 -r f132a4fd8679 src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Tue Feb 16 13:35:42 2010 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Tue Feb 16 14:08:39 2010 +0100 @@ -68,17 +68,6 @@ quote_tr' (Syntax.const name) (t :: ts) | bexp_tr' _ _ = raise Match; - fun upd_tr' (x_upd, T) = - (case try (unsuffix Record.updateN) x_upd of - SOME x => (x, if T = dummyT then T else Term.domain_type T) - | NONE => raise Match); - - fun update_name_tr' (Free x) = Free (upd_tr' x) - | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) = - c $ Free (upd_tr' x) - | update_name_tr' (Const x) = Const (upd_tr' x) - | update_name_tr' _ = raise Match; - fun K_tr' (Abs (_, _, t)) = if null (loose_bnos t) then t else raise Match | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = @@ -86,7 +75,7 @@ | K_tr' _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f) + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) (Abs (x, dummyT, K_tr' k) :: ts) | assign_tr' _ = raise Match; in diff -r 8b8302da3a55 -r f132a4fd8679 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Tue Feb 16 13:35:42 2010 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Feb 16 14:08:39 2010 +0100 @@ -260,23 +260,14 @@ quote_tr' (Syntax.const name) (t :: ts) | bexp_tr' _ _ = raise Match; - fun upd_tr' (x_upd, T) = - (case try (unsuffix Record.updateN) x_upd of - SOME x => (x, if T = dummyT then T else Term.domain_type T) - | NONE => raise Match); - - fun update_name_tr' (Free x) = Free (upd_tr' x) - | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) = - c $ Free (upd_tr' x) - | update_name_tr' (Const x) = Const (upd_tr' x) - | update_name_tr' _ = raise Match; - - fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match - | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match + fun K_tr' (Abs (_, _, t)) = + if null (loose_bnos t) then t else raise Match + | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = + if null (loose_bnos t) then t else raise Match | K_tr' _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = - quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f) + quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) (Abs (x, dummyT, K_tr' k) :: ts) | assign_tr' _ = raise Match; in diff -r 8b8302da3a55 -r f132a4fd8679 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Feb 16 13:35:42 2010 +0100 +++ b/src/HOL/Record.thy Tue Feb 16 14:08:39 2010 +0100 @@ -437,7 +437,6 @@ "_record" :: "fields => 'a" ("(3'(| _ |'))") "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") - "_update_name" :: idt "_update" :: "ident => 'a => update" ("(2_ :=/ _)") "" :: "update => updates" ("_") "_updates" :: "update => updates => updates" ("_,/ _") diff -r 8b8302da3a55 -r f132a4fd8679 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Feb 16 13:35:42 2010 +0100 +++ b/src/HOL/Tools/record.ML Tue Feb 16 14:08:39 2010 +0100 @@ -730,13 +730,6 @@ end; -fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix updateN x, T), ts) - | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix updateN x, T), ts) - | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) = - (* FIXME @{type_syntax} *) - list_comb (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts) - | update_name_tr ts = raise TERM ("update_name_tr", ts); - fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) = if c = mark then (name, arg) else raise TERM ("dest_ext_field: " ^ mark, [t]) @@ -855,8 +848,7 @@ val parse_translation = - [(@{syntax_const "_record_update"}, record_update_tr), - (@{syntax_const "_update_name"}, update_name_tr)]; + [(@{syntax_const "_record_update"}, record_update_tr)]; val adv_parse_translation = [(@{syntax_const "_record"}, adv_record_tr), diff -r 8b8302da3a55 -r f132a4fd8679 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Feb 16 13:35:42 2010 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Tue Feb 16 14:08:39 2010 +0100 @@ -19,6 +19,7 @@ val antiquote_tr': string -> term -> term val quote_tr': string -> term -> term val quote_antiquote_tr': string -> string -> string -> string * (term list -> term) + val update_name_tr': term -> term val mark_bound: string -> term val mark_boundT: string * typ -> term val bound_vars: (string * typ) list -> term -> term @@ -187,6 +188,15 @@ in (quoteN, tr) end; +(* corresponding updates *) + +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts) + | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts) + | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = + list_comb (c $ update_name_tr [t] $ (Lexicon.const "fun" $ ty $ Lexicon.const "dummy"), ts) + | update_name_tr ts = raise TERM ("update_name_tr", ts); + + (* indexed syntax *) fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast @@ -444,6 +454,19 @@ in (name, tr') end; +(* corresponding updates *) + +fun upd_tr' (x_upd, T) = + (case try (unsuffix "_update") x_upd of + SOME x => (x, if T = dummyT then T else Term.domain_type T) + | NONE => raise Match); + +fun update_name_tr' (Free x) = Free (upd_tr' x) + | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x) + | update_name_tr' (Const x) = Const (upd_tr' x) + | update_name_tr' _ = raise Match; + + (* indexed syntax *) fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast @@ -468,17 +491,31 @@ (** Pure translations **) val pure_trfuns = - ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr), - ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_idtypdummy", idtypdummy_ast_tr), - ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr), - ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)], - [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), - ("_sort_constraint", sort_constraint_tr), ("_TYPE", type_tr), - ("_DDDOT", dddot_tr), ("_index", index_tr)], - ([]: (string * (term list -> term)) list), - [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), - ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'), - ("_index", index_ast_tr')]); + ([("_constify", constify_ast_tr), + ("_appl", appl_ast_tr), + ("_applC", applC_ast_tr), + ("_lambda", lambda_ast_tr), + ("_idtyp", idtyp_ast_tr), + ("_idtypdummy", idtypdummy_ast_tr), + ("_bigimpl", bigimpl_ast_tr), + ("_indexdefault", indexdefault_ast_tr), + ("_indexnum", indexnum_ast_tr), + ("_indexvar", indexvar_ast_tr), + ("_struct", struct_ast_tr)], + [("_abs", abs_tr), + ("_aprop", aprop_tr), + ("_ofclass", ofclass_tr), + ("_sort_constraint", sort_constraint_tr), + ("_TYPE", type_tr), + ("_DDDOT", dddot_tr), + ("_update_name", update_name_tr), + ("_index", index_tr)], + [], + [("_abs", abs_ast_tr'), + ("_idts", idtyp_ast_tr' "_idts"), + ("_pttrns", idtyp_ast_tr' "_pttrns"), + ("==>", impl_ast_tr'), + ("_index", index_ast_tr')]); val pure_trfunsT = [("_type_prop", type_prop_tr'), ("TYPE", type_tr'), ("_type_constraint_", type_constraint_tr')]; diff -r 8b8302da3a55 -r f132a4fd8679 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Feb 16 13:35:42 2010 +0100 +++ b/src/Pure/pure_thy.ML Tue Feb 16 14:08:39 2010 +0100 @@ -309,6 +309,7 @@ ("_indexdefault", typ "index", Delimfix ""), ("_indexvar", typ "index", Delimfix "'\\"), ("_struct", typ "index => logic", Mixfix ("\\_", [1000], 1000)), + ("_update_name", typ "idt", NoSyn), ("==>", typ "prop => prop => prop", Delimfix "op ==>"), (Term.dummy_patternN, typ "aprop", Delimfix "'_"), ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),