--- 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;
--- 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
--- 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
--- 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" ("_,/ _")
--- 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),
--- 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')];
--- 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 "'\\<index>"),
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [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'(_')))"),