# HG changeset patch # User wenzelm # Date 1266349364 -3600 # Node ID 3011b2149089b11e1266daa01a8b029226a68edf # Parent 52ab455915d85f8022a0f6426bcaf77ebeae4b94# Parent eee63670b5aa7786c2b05aefe3f88c1d5d2f342b merged diff -r 52ab455915d8 -r 3011b2149089 src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Tue Feb 16 16:20:46 2010 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Tue Feb 16 20:42:44 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 52ab455915d8 -r 3011b2149089 src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Tue Feb 16 16:20:46 2010 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Tue Feb 16 20:42:44 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 52ab455915d8 -r 3011b2149089 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Tue Feb 16 16:20:46 2010 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Feb 16 20:42:44 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 52ab455915d8 -r 3011b2149089 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Feb 16 16:20:46 2010 +0100 +++ b/src/HOL/Record.thy Tue Feb 16 20:42:44 2010 +0100 @@ -420,35 +420,34 @@ subsection {* Concrete record syntax *} nonterminals - ident field_type field_types field fields update updates + ident field_type field_types field fields field_update field_updates syntax "_constify" :: "id => ident" ("_") "_constify" :: "longid => ident" ("_") - "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") + "_field_type" :: "ident => type => field_type" ("(2_ ::/ _)") "" :: "field_type => field_types" ("_") - "_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") + "_field_types" :: "field_type => field_types => field_types" ("_,/ _") "_record_type" :: "field_types => type" ("(3'(| _ |'))") - "_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") + "_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))") - "_field" :: "[ident, 'a] => field" ("(2_ =/ _)") + "_field" :: "ident => 'a => field" ("(2_ =/ _)") "" :: "field => fields" ("_") - "_fields" :: "[field, fields] => fields" ("_,/ _") + "_fields" :: "field => fields => fields" ("_,/ _") "_record" :: "fields => 'a" ("(3'(| _ |'))") - "_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") + "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") - "_update_name" :: idt - "_update" :: "ident => 'a => update" ("(2_ :=/ _)") - "" :: "update => updates" ("_") - "_updates" :: "update => updates => updates" ("_,/ _") - "_record_update" :: "'a => updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) + "_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)") + "" :: "field_update => field_updates" ("_") + "_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _") + "_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) syntax (xsymbols) "_record_type" :: "field_types => type" ("(3\_\)") "_record_type_scheme" :: "field_types => type => type" ("(3\_,/ (2\ ::/ _)\)") "_record" :: "fields => 'a" ("(3\_\)") "_record_scheme" :: "fields => 'a => 'a" ("(3\_,/ (2\ =/ _)\)") - "_record_update" :: "'a => updates => 'b" ("_/(3\_\)" [900, 0] 900) + "_record_update" :: "'a => field_updates => 'b" ("_/(3\_\)" [900, 0] 900) subsection {* Record package *} diff -r 52ab455915d8 -r 3011b2149089 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Tue Feb 16 20:42:44 2010 +0100 @@ -146,7 +146,7 @@ (replicate (length rstp) "x") in [((prfx, gvars @ map Free (xs ~~ Ts)), - (Const (@{const_name HOL.undefined}, res_ty), (~1, false)))] + (Const (@{const_syntax undefined}, res_ty), (~1, false)))] end else in_group in @@ -315,7 +315,7 @@ fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used = let val (t', used') = prep_pat t used in (c $ t' $ tT, used') end - | prep_pat (Const (@{const_name dummy_pattern}, T)) used = + | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used = let val x = Name.variant used "x" in (Free (x, T), x :: used) end | prep_pat (Const (s, T)) used = @@ -381,7 +381,7 @@ fun count_cases (_, _, true) = I | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c); - val is_undefined = name_of #> equal (SOME @{const_name HOL.undefined}); + val is_undefined = name_of #> equal (SOME @{const_syntax undefined}); fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body) in case ty_info tab cname of SOME {constructors, case_name} => @@ -399,7 +399,7 @@ (fold_rev count_cases cases []); val R = type_of t; val dummy = - if d then Const (@{const_name dummy_pattern}, R) + if d then Const (@{const_syntax dummy_pattern}, R) else Free (Name.variant used "x", R) in SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of diff -r 52ab455915d8 -r 3011b2149089 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/HOL/Tools/record.ML Tue Feb 16 20:42:44 2010 +0100 @@ -153,7 +153,8 @@ val ([isom_def], cdef_thy) = typ_thy |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)] - |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; + |> PureThy.add_defs false + [Thm.no_attributes (apfst (Binding.conceal o Binding.name) isom_spec)]; val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro)); val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT); @@ -269,11 +270,9 @@ val Trueprop = HOLogic.mk_Trueprop; fun All xs t = Term.list_all_free (xs, t); -infix 9 $$; infix 0 :== ===; infixr 0 ==>; -val op $$ = Term.list_comb; val op :== = Primitive_Defs.mk_defpair; val op === = Trueprop o HOLogic.mk_eq; val op ==> = Logic.mk_implies; @@ -585,9 +584,9 @@ let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; - val data = make_record_data records sel_upd - equalities extinjects (Symtab.update_new (name, thm) extsplit) splits - extfields fieldext; + val data = + make_record_data records sel_upd equalities extinjects + (Symtab.update_new (name, thm) extsplit) splits extfields fieldext; in Records_Data.put data thy end; @@ -597,9 +596,9 @@ let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; - val data = make_record_data records sel_upd - equalities extinjects extsplit (Symtab.update_new (name, thmP) splits) - extfields fieldext; + val data = + make_record_data records sel_upd equalities extinjects extsplit + (Symtab.update_new (name, thmP) splits) extfields fieldext; in Records_Data.put data thy end; val get_splits = Symtab.lookup o #splits o Records_Data.get; @@ -618,8 +617,7 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; val data = - make_record_data records sel_upd - equalities extinjects extsplit splits + make_record_data records sel_upd equalities extinjects extsplit splits (Symtab.update_new (name, fields) extfields) fieldext; in Records_Data.put data thy end; @@ -634,20 +632,20 @@ val midx = maxidx_of_typs (moreT :: Ts); val varifyT = varifyT midx; val {records, extfields, ...} = Records_Data.get thy; - val (flds, (more, _)) = split_last (Symtab.lookup_list extfields name); + val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name); val args = map varifyT (snd (#extension (the (Symtab.lookup records recname)))); - val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty); - val flds' = map (apsnd (Envir.norm_type subst o varifyT)) flds; - in (flds', (more, moreT)) end; + val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) Vartab.empty; + val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields; + in (fields', (more, moreT)) end; fun get_recT_fields thy T = let - val (root_flds, (root_more, root_moreT)) = get_extT_fields thy T; - val (rest_flds, rest_more) = + val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T; + val (rest_fields, rest_more) = if is_recT root_moreT then get_recT_fields thy root_moreT else ([], (root_more, root_moreT)); - in (root_flds @ rest_flds, rest_more) end; + in (root_fields @ rest_fields, rest_more) end; (* access 'fieldext' *) @@ -700,7 +698,8 @@ fun decode_type thy t = let - fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy); + fun get_sort env xi = + the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname)); val map_sort = Sign.intern_sort thy; in Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t @@ -710,155 +709,138 @@ (* parse translations *) -fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = - if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg) - else raise TERM ("gen_field_tr: " ^ mark, [t]) - | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); - -fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) = - if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u - else [gen_field_tr mark sfx tm] - | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm]; - - -fun record_update_tr [t, u] = - fold (curry op $) - (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t - | record_update_tr ts = raise TERM ("record_update_tr", ts); - -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts - | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts - | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) = - (* FIXME @{type_syntax} *) - (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]) - | dest_ext_field _ t = raise TERM ("dest_ext_field", [t]); - -fun dest_ext_fields sep mark (trm as (Const (c, _) $ t $ u)) = - if c = sep then dest_ext_field mark t :: dest_ext_fields sep mark u - else [dest_ext_field mark trm] - | dest_ext_fields _ mark t = [dest_ext_field mark t]; - -fun gen_ext_fields_tr sep mark sfx more ctxt t = +local + +fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) = + (name, arg) + | field_type_tr t = raise TERM ("field_type_tr", [t]); + +fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) = + field_type_tr t :: field_types_tr u + | field_types_tr t = [field_type_tr t]; + +fun record_field_types_tr more ctxt t = let val thy = ProofContext.theory_of ctxt; - fun err msg = raise TERM ("error in record input: " ^ msg, [t]); - - val fieldargs = dest_ext_fields sep mark t; - fun splitargs (field :: fields) ((name, arg) :: fargs) = - if can (unsuffix name) field - then - let val (args, rest) = splitargs fields fargs + fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]); + + fun split_args (field :: fields) ((name, arg) :: fargs) = + if can (unsuffix name) field then + let val (args, rest) = split_args fields fargs in (arg :: args, rest) end else err ("expecting field " ^ field ^ " but got " ^ name) - | splitargs [] (fargs as (_ :: _)) = ([], fargs) - | splitargs (_ :: _) [] = err "expecting more fields" - | splitargs _ _ = ([], []); - - fun mk_ext (fargs as (name, _) :: _) = - (case get_fieldext thy (Sign.intern_const thy name) of - SOME (ext, _) => - (case get_extfields thy ext of - SOME flds => - let - val (args, rest) = splitargs (map fst (but_last flds)) fargs; - val more' = mk_ext rest; - in list_comb (Syntax.const (suffix sfx ext), args @ [more']) end - | NONE => err ("no fields defined for " ^ ext)) - | NONE => err (name ^ " is no proper field")) - | mk_ext [] = more; - in mk_ext fieldargs end; - -fun gen_ext_type_tr sep mark sfx more ctxt t = - let - val thy = ProofContext.theory_of ctxt; - fun err msg = raise TERM ("error in record-type input: " ^ msg, [t]); - - val fieldargs = dest_ext_fields sep mark t; - fun splitargs (field :: fields) ((name, arg) :: fargs) = - if can (unsuffix name) field then - let val (args, rest) = splitargs fields fargs - in (arg :: args, rest) end - else err ("expecting field " ^ field ^ " but got " ^ name) - | splitargs [] (fargs as (_ :: _)) = ([], fargs) - | splitargs (_ :: _) [] = err "expecting more fields" - | splitargs _ _ = ([], []); + | split_args [] (fargs as (_ :: _)) = ([], fargs) + | split_args (_ :: _) [] = err "expecting more fields" + | split_args _ _ = ([], []); fun mk_ext (fargs as (name, _) :: _) = (case get_fieldext thy (Sign.intern_const thy name) of SOME (ext, alphas) => (case get_extfields thy ext of - SOME flds => - (let - val flds' = but_last flds; - val types = map snd flds'; - val (args, rest) = splitargs (map fst flds') fargs; + SOME fields => + let + val fields' = but_last fields; + val types = map snd fields'; + val (args, rest) = split_args (map fst fields') fargs; val argtypes = map (Sign.certify_typ thy o decode_type thy) args; val midx = fold Term.maxidx_typ argtypes 0; val varifyT = varifyT midx; val vartypes = map varifyT types; - val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty; + val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty + handle Type.TYPE_MATCH => err "type is no proper record (extension)"; val alphas' = map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT) (but_last alphas); val more' = mk_ext rest; in - list_comb (Syntax.const (suffix sfx ext), alphas' @ [more']) - end handle Type.TYPE_MATCH => - raise err "type is no proper record (extension)") + (* FIXME authentic syntax *) + list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more']) + end | NONE => err ("no fields defined for " ^ ext)) | NONE => err (name ^ " is no proper field")) | mk_ext [] = more; - - in mk_ext fieldargs end; - -fun gen_adv_record_tr sep mark sfx unit ctxt [t] = - gen_ext_fields_tr sep mark sfx unit ctxt t - | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); - -fun gen_adv_record_scheme_tr sep mark sfx ctxt [t, more] = - gen_ext_fields_tr sep mark sfx more ctxt t - | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); - -fun gen_adv_record_type_tr sep mark sfx unit ctxt [t] = - gen_ext_type_tr sep mark sfx unit ctxt t - | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); - -fun gen_adv_record_type_scheme_tr sep mark sfx ctxt [t, more] = - gen_ext_type_tr sep mark sfx more ctxt t - | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); - -val adv_record_tr = - gen_adv_record_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN HOLogic.unit; - -val adv_record_scheme_tr = - gen_adv_record_scheme_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN; - -val adv_record_type_tr = - gen_adv_record_type_tr - @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN - (Syntax.term_of_typ false (HOLogic.unitT)); - -val adv_record_type_scheme_tr = - gen_adv_record_type_scheme_tr - @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN; - + in + mk_ext (field_types_tr t) + end; + +(* FIXME @{type_syntax} *) +fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t + | record_type_tr _ ts = raise TERM ("record_type_tr", ts); + +fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t + | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts); + + +fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg) + | field_tr t = raise TERM ("field_tr", [t]); + +fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u + | fields_tr t = [field_tr t]; + +fun record_fields_tr more ctxt t = + let + val thy = ProofContext.theory_of ctxt; + fun err msg = raise TERM ("Error in record input: " ^ msg, [t]); + + fun split_args (field :: fields) ((name, arg) :: fargs) = + if can (unsuffix name) field + then + let val (args, rest) = split_args fields fargs + in (arg :: args, rest) end + else err ("expecting field " ^ field ^ " but got " ^ name) + | split_args [] (fargs as (_ :: _)) = ([], fargs) + | split_args (_ :: _) [] = err "expecting more fields" + | split_args _ _ = ([], []); + + fun mk_ext (fargs as (name, _) :: _) = + (case get_fieldext thy (Sign.intern_const thy name) of + SOME (ext, _) => + (case get_extfields thy ext of + SOME fields => + let + val (args, rest) = split_args (map fst (but_last fields)) fargs; + val more' = mk_ext rest; + in + (* FIXME authentic syntax *) + list_comb (Syntax.const (suffix extN ext), args @ [more']) + end + | NONE => err ("no fields defined for " ^ ext)) + | NONE => err (name ^ " is no proper field")) + | mk_ext [] = more; + in mk_ext (fields_tr t) end; + +fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t + | record_tr _ ts = raise TERM ("record_tr", ts); + +fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t + | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); + + +fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) = + Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg) + | field_update_tr t = raise TERM ("field_update_tr", [t]); + +fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) = + field_update_tr t :: field_updates_tr u + | field_updates_tr t = [field_update_tr t]; + +fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t + | record_update_tr ts = raise TERM ("record_update_tr", ts); + +in val parse_translation = - [(@{syntax_const "_record_update"}, record_update_tr), - (@{syntax_const "_update_name"}, update_name_tr)]; - -val adv_parse_translation = - [(@{syntax_const "_record"}, adv_record_tr), - (@{syntax_const "_record_scheme"}, adv_record_scheme_tr), - (@{syntax_const "_record_type"}, adv_record_type_tr), - (@{syntax_const "_record_type_scheme"}, adv_record_type_scheme_tr)]; + [(@{syntax_const "_record_update"}, record_update_tr)]; + +val advanced_parse_translation = + [(@{syntax_const "_record"}, record_tr), + (@{syntax_const "_record_scheme"}, record_scheme_tr), + (@{syntax_const "_record_type"}, record_type_tr), + (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)]; + +end; (* print translations *) @@ -866,7 +848,9 @@ val print_record_type_abbr = Unsynchronized.ref true; val print_record_type_as_fields = Unsynchronized.ref true; -fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) = +local + +fun field_updates_tr' (tm as Const (c, _) $ k $ u) = let val t = (case k of @@ -876,79 +860,139 @@ if null (loose_bnos t) then t else raise Match | _ => raise Match); in - (case try (unsuffix sfx) name_field of + (case try (unsuffix updateN) c of SOME name => - apfst (cons (Syntax.const mark $ Syntax.free name $ t)) - (gen_field_upds_tr' mark sfx u) + (* FIXME check wrt. record data (??) *) + (* FIXME early extern (!??) *) + apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t)) + (field_updates_tr' u) | NONE => ([], tm)) end - | gen_field_upds_tr' _ _ tm = ([], tm); + | field_updates_tr' tm = ([], tm); fun record_update_tr' tm = - let val (ts, u) = gen_field_upds_tr' @{syntax_const "_update"} updateN tm in - if null ts then raise Match - else + (case field_updates_tr' tm of + ([], _) => raise Match + | (ts, u) => Syntax.const @{syntax_const "_record_update"} $ u $ - foldr1 (fn (v, w) => Syntax.const @{syntax_const "_updates"} $ v $ w) (rev ts) - end; - -fun gen_field_tr' sfx tr' name = - let val name_sfx = suffix sfx name - in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; - -fun record_tr' sep mark record record_scheme unit ctxt t = + foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts)); + +in + +fun field_update_tr' name = + let + (* FIXME authentic syntax *) + val update_name = suffix updateN name; + fun tr' [t, u] = record_update_tr' (Syntax.const update_name $ t $ u) + | tr' _ = raise Match; + in (update_name, tr') end; + +end; + + +local + +(* FIXME early extern (!??) *) +(* FIXME Syntax.free (??) *) +fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t; + +fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u; + +fun record_tr' ctxt t = let val thy = ProofContext.theory_of ctxt; - fun field_lst t = + fun strip_fields t = (case strip_comb t of (Const (ext, _), args as (_ :: _)) => - (case try (unsuffix extN) (Sign.intern_const thy ext) of + (case try (unsuffix extN) (Sign.intern_const thy ext) of (* FIXME authentic syntax *) SOME ext' => (case get_extfields thy ext' of - SOME flds => + SOME fields => (let - val f :: fs = but_last (map fst flds); - val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs; + val f :: fs = but_last (map fst fields); + val fields' = Sign.extern_const thy f :: map Long_Name.base_name fs; val (args', more) = split_last args; - in (flds' ~~ args') @ field_lst more end + in (fields' ~~ args') @ strip_fields more end handle Library.UnequalLengths => [("", t)]) | NONE => [("", t)]) | NONE => [("", t)]) | _ => [("", t)]); - val (flds, (_, more)) = split_last (field_lst t); - val _ = if null flds then raise Match else (); - val flds' = map (fn (n, t) => Syntax.const mark $ Syntax.const n $ t) flds; - val flds'' = foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds'; + val (fields, (_, more)) = split_last (strip_fields t); + val _ = null fields andalso raise Match; + val u = foldr1 fields_tr' (map field_tr' fields); in - if unit more - then Syntax.const record $ flds'' - else Syntax.const record_scheme $ flds'' $ more + case more of + Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u + | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more end; -fun gen_record_tr' name = +in + +fun record_ext_tr' name = + let + val ext_name = suffix extN name; + fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts)); + in (ext_name, tr') end; + +end; + + +local + +(* FIXME early extern (!??) *) +(* FIXME Syntax.free (??) *) +fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t; + +fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u; + +fun record_type_tr' ctxt t = let - val name_sfx = suffix extN name; - val unit = fn Const (@{const_syntax Product_Type.Unity}, _) => true | _ => false; - fun tr' ctxt ts = - record_tr' - @{syntax_const "_fields"} - @{syntax_const "_field"} - @{syntax_const "_record"} - @{syntax_const "_record_scheme"} - unit ctxt (list_comb (Syntax.const name_sfx, ts)); - in (name_sfx, tr') end; - -fun print_translation names = - map (gen_field_tr' updateN record_update_tr') names; - - -(* record_type_abbr_tr' *) + val thy = ProofContext.theory_of ctxt; + + val T = decode_type thy t; + val varifyT = varifyT (Term.maxidx_of_typ T); + + val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy; + + fun strip_fields T = + (case T of + Type (ext, args) => + (case try (unsuffix ext_typeN) ext of + SOME ext' => + (case get_extfields thy ext' of + SOME fields => + (case get_fieldext thy (fst (hd fields)) of + SOME (_, alphas) => + (let + val f :: fs = but_last fields; + val fields' = + apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs; + val (args', more) = split_last args; + val alphavars = map varifyT (but_last alphas); + val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty; + val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields'; + in fields'' @ strip_fields more end + handle Type.TYPE_MATCH => [("", T)] + | Library.UnequalLengths => [("", T)]) + | NONE => [("", T)]) + | NONE => [("", T)]) + | NONE => [("", T)]) + | _ => [("", T)]); + + val (fields, (_, moreT)) = split_last (strip_fields T); + val _ = null fields andalso raise Match; + val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields); + in + if not (! print_record_type_as_fields) orelse null fields then raise Match + else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u + else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT + end; (*try to reconstruct the record name type abbreviation from the (nested) extension types*) -fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm = +fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm = let val thy = ProofContext.theory_of ctxt; @@ -984,89 +1028,35 @@ if ! print_record_type_abbr then (case last_extT T of SOME (name, _) => - if name = lastExt then - (let val subst = match schemeT T in + if name = last_ext then + let val subst = match schemeT T in if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy)))) then mk_type_abbr subst abbr alphas else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta]) - end handle Type.TYPE_MATCH => default_tr' ctxt tm) + end handle Type.TYPE_MATCH => record_type_tr' ctxt tm else raise Match (*give print translation of specialised record a chance*) | _ => raise Match) - else default_tr' ctxt tm + else record_type_tr' ctxt tm end; -fun record_type_tr' sep mark record record_scheme ctxt t = +in + +fun record_ext_type_tr' name = let - val thy = ProofContext.theory_of ctxt; - - val T = decode_type thy t; - val varifyT = varifyT (Term.maxidx_of_typ T); - - fun term_of_type T = Syntax.term_of_typ (! Syntax.show_sorts) (Sign.extern_typ thy T); - - fun field_lst T = - (case T of - Type (ext, args) => - (case try (unsuffix ext_typeN) ext of - SOME ext' => - (case get_extfields thy ext' of - SOME flds => - (case get_fieldext thy (fst (hd flds)) of - SOME (_, alphas) => - (let - val f :: fs = but_last flds; - val flds' = apfst (Sign.extern_const thy) f :: - map (apfst Long_Name.base_name) fs; - val (args', more) = split_last args; - val alphavars = map varifyT (but_last alphas); - val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty; - val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds'; - in flds'' @ field_lst more end - handle Type.TYPE_MATCH => [("", T)] - | Library.UnequalLengths => [("", T)]) - | NONE => [("", T)]) - | NONE => [("", T)]) - | NONE => [("", T)]) - | _ => [("", T)]); - - val (flds, (_, moreT)) = split_last (field_lst T); - val flds' = map (fn (n, T) => Syntax.const mark $ Syntax.const n $ term_of_type T) flds; - val flds'' = - foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds' - handle Empty => raise Match; - in - if not (! print_record_type_as_fields) orelse null flds then raise Match - else if moreT = HOLogic.unitT then Syntax.const record $ flds'' - else Syntax.const record_scheme $ flds'' $ term_of_type moreT - end; - - -fun gen_record_type_tr' name = + val ext_type_name = suffix ext_typeN name; + fun tr' ctxt ts = + record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts)); + in (ext_type_name, tr') end; + +fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name = let - val name_sfx = suffix ext_typeN name; + val ext_type_name = suffix ext_typeN name; fun tr' ctxt ts = - record_type_tr' - @{syntax_const "_field_types"} - @{syntax_const "_field_type"} - @{syntax_const "_record_type"} - @{syntax_const "_record_type_scheme"} - ctxt (list_comb (Syntax.const name_sfx, ts)); - in (name_sfx, tr') end; - - -fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name = - let - val name_sfx = suffix ext_typeN name; - val default_tr' = - record_type_tr' - @{syntax_const "_field_types"} - @{syntax_const "_field_type"} - @{syntax_const "_record_type"} - @{syntax_const "_record_type_scheme"}; - fun tr' ctxt ts = - record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt - (list_comb (Syntax.const name_sfx, ts)); - in (name_sfx, tr') end; + record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt + (list_comb (Syntax.const ext_type_name, ts)); + in (ext_type_name, tr') end; + +end; @@ -1448,8 +1438,8 @@ (fn thy => fn _ => fn t => (case t of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => - if quantifier = @{const_name All} orelse - quantifier = @{const_name all} orelse + if quantifier = @{const_name all} orelse + quantifier = @{const_name All} orelse quantifier = @{const_name Ex} then (case rec_id ~1 T of @@ -1573,20 +1563,20 @@ (* record_split_tac *) -(*Split all records in the goal, which are quantified by ALL or !!.*) +(*Split all records in the goal, which are quantified by !! or ALL.*) val record_split_tac = CSUBGOAL (fn (cgoal, i) => let val goal = term_of cgoal; val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = @{const_name All} orelse s = @{const_name all}) andalso is_recT T + (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T | _ => false); fun is_all t = (case t of Const (quantifier, _) $ _ => - if quantifier = @{const_name All} orelse quantifier = @{const_name all} then ~1 else 0 + if quantifier = @{const_name all} orelse quantifier = @{const_name All} then ~1 else 0 | _ => 0); in if has_rec goal then @@ -1989,25 +1979,24 @@ (* prepare print translation functions *) - - val field_tr's = - print_translation (distinct (op =) (maps external_names (full_moreN :: names))); - - val adv_ext_tr's = - let val trnames = external_names extN - in map (gen_record_tr') trnames end; - - val adv_record_type_abbr_tr's = + (* FIXME authentic syntax *) + + val field_update_tr's = + map field_update_tr' (distinct (op =) (maps external_names (full_moreN :: names))); + + val record_ext_tr's = map record_ext_tr' (external_names extN); + + val record_ext_type_abbr_tr's = let val trnames = external_names (hd extension_names); - val lastExt = unsuffix ext_typeN (fst extension); - in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames end; - - val adv_record_type_tr's = + val last_ext = unsuffix ext_typeN (fst extension); + in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end; + + val record_ext_type_tr's = let + (*avoid conflict with record_type_abbr_tr's*) val trnames = if parent_len > 0 then external_names extN else []; - (*avoid conflict with adv_record_type_abbr_tr's*) - in map (gen_record_type_tr') trnames end; + in map record_ext_type_tr' trnames end; (* prepare declarations *) @@ -2024,8 +2013,8 @@ (*record (scheme) type abbreviation*) val recordT_specs = - [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), - (b, alphas, recT0, Syntax.NoSyn)]; + [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, NoSyn), + (b, alphas, recT0, NoSyn)]; val ext_defs = ext_def :: map #ext_def parents; @@ -2090,36 +2079,40 @@ val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms); (*derived operations*) - val make_spec = Const (full (Binding.name makeN), all_types ---> recT0) $$ all_vars :== - mk_rec (all_vars @ [HOLogic.unit]) 0; - val fields_spec = Const (full (Binding.name fields_selN), types ---> Type extension) $$ vars :== - mk_rec (all_vars @ [HOLogic.unit]) parent_len; + val make_spec = + list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :== + mk_rec (all_vars @ [HOLogic.unit]) 0; + val fields_spec = + list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :== + mk_rec (all_vars @ [HOLogic.unit]) parent_len; val extend_spec = Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :== - mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; - val truncate_spec = Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :== - mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; + mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; + val truncate_spec = + Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :== + mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; (* 2st stage: defs_thy *) fun mk_defs () = extension_thy - |> Sign.add_trfuns ([], [], field_tr's, []) + |> Sign.add_trfuns ([], [], field_update_tr's, []) |> Sign.add_advanced_trfuns - ([], [], adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's, []) + ([], [], record_ext_tr's @ record_ext_type_tr's @ record_ext_type_abbr_tr's, []) |> Sign.parent_path |> Sign.add_tyabbrs_i recordT_specs |> Sign.add_path base_name |> Sign.add_consts_i - (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx)) - sel_decls (field_syntax @ [Syntax.NoSyn])) - |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn))) + (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx)) sel_decls (field_syntax @ [NoSyn])) + |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, NoSyn))) (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) - |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs) - ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs) - ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) - [make_spec, fields_spec, extend_spec, truncate_spec]) + |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) + sel_specs + ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) + upd_specs + ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) + [make_spec, fields_spec, extend_spec, truncate_spec] |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => fold Code.add_default_eqn sel_defs @@ -2512,7 +2505,7 @@ val setup = Sign.add_trfuns ([], parse_translation, [], []) #> - Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #> + Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #> Simplifier.map_simpset (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); diff -r 52ab455915d8 -r 3011b2149089 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/Pure/Isar/expression.ML Tue Feb 16 20:42:44 2010 +0100 @@ -606,7 +606,7 @@ fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => if length args = n then - Syntax.const "_aprop" $ + Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) else raise Match); diff -r 52ab455915d8 -r 3011b2149089 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Feb 16 20:42:44 2010 +0100 @@ -332,16 +332,14 @@ val print_abbrevs = Toplevel.unknown_context o Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of); -val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => - ProofContext.setmp_verbose_CRITICAL - ProofContext.print_lthms (Toplevel.context_of state)); +val print_facts = Toplevel.unknown_context o + Toplevel.keep (ProofContext.print_lthms o Toplevel.context_of); -val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state => - Attrib.print_configs (Toplevel.context_of state)); +val print_configs = Toplevel.unknown_context o + Toplevel.keep (Attrib.print_configs o Toplevel.context_of); -val print_theorems_proof = Toplevel.keep (fn state => - ProofContext.setmp_verbose_CRITICAL - ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state))); +val print_theorems_proof = + Toplevel.keep (ProofContext.print_lthms o Proof.context_of o Toplevel.proof_of); fun print_theorems_theory verbose = Toplevel.keep (fn state => Toplevel.theory_of state |> @@ -430,11 +428,11 @@ (* print proof context contents *) -val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => - ProofContext.setmp_verbose_CRITICAL ProofContext.print_binds (Toplevel.context_of state)); +val print_binds = Toplevel.unknown_context o + Toplevel.keep (ProofContext.print_binds o Toplevel.context_of); -val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state => - ProofContext.setmp_verbose_CRITICAL ProofContext.print_cases (Toplevel.context_of state)); +val print_cases = Toplevel.unknown_context o + Toplevel.keep (ProofContext.print_cases o Toplevel.context_of); (* print theorems, terms, types etc. *) diff -r 52ab455915d8 -r 3011b2149089 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Feb 16 20:42:44 2010 +0100 @@ -30,7 +30,6 @@ val consts_of: Proof.context -> Consts.T val const_syntax_name: Proof.context -> string -> string val the_const_constraint: Proof.context -> string -> typ - val mk_const: Proof.context -> string * typ list -> term val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context val facts_of: Proof.context -> Facts.T @@ -123,14 +122,13 @@ val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context - val verbose: bool Unsynchronized.ref - val setmp_verbose_CRITICAL: ('a -> 'b) -> 'a -> 'b val print_syntax: Proof.context -> unit val print_abbrevs: Proof.context -> unit val print_binds: Proof.context -> unit val print_lthms: Proof.context -> unit val print_cases: Proof.context -> unit val debug: bool Unsynchronized.ref + val verbose: bool Unsynchronized.ref val prems_limit: int Unsynchronized.ref val pretty_ctxt: Proof.context -> Pretty.T list val pretty_context: Proof.context -> Pretty.T list @@ -240,8 +238,6 @@ val const_syntax_name = Consts.syntax_name o consts_of; val the_const_constraint = Consts.the_constraint o consts_of; -fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts)); - val facts_of = #facts o rep_context; val cases_of = #cases o rep_context; @@ -1198,14 +1194,6 @@ (** print context information **) -val debug = Unsynchronized.ref false; - -val verbose = Unsynchronized.ref false; -fun verb f x = if ! verbose then f (x ()) else []; - -fun setmp_verbose_CRITICAL f x = setmp_CRITICAL verbose true f x; - - (* local syntax *) val print_syntax = Syntax.print_syntax o syn_of; @@ -1223,7 +1211,7 @@ else cons (c, Logic.mk_equals (Const (c, T), t)); val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts [])); in - if null abbrevs andalso not (! verbose) then [] + if null abbrevs then [] else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] end; @@ -1237,7 +1225,7 @@ val binds = Variable.binds_of ctxt; fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t)); in - if Vartab.is_empty binds andalso not (! verbose) then [] + if Vartab.is_empty binds then [] else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))] end; @@ -1251,10 +1239,10 @@ val local_facts = facts_of ctxt; val props = Facts.props local_facts; val facts = - (if null props then [] else [("unnamed", props)]) @ + (if null props then [] else [("", props)]) @ Facts.dest_static [] local_facts; in - if null facts andalso not (! verbose) then [] + if null facts then [] else [Pretty.big_list "facts:" (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) facts)))] end; @@ -1277,8 +1265,9 @@ ((if a = "" then [] else [Pretty.str (a ^ ":")]) @ map (Pretty.quote o prt_term) ts)); fun prt_sect _ _ _ [] = [] - | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s :: - flat (Library.separate sep (map (Library.single o prt) xs))))]; + | prt_sect s sep prt xs = + [Pretty.block (Pretty.breaks (Pretty.str s :: + flat (separate sep (map (single o prt) xs))))]; in Pretty.block (Pretty.fbreaks (Pretty.str (name ^ ":") :: @@ -1299,7 +1288,7 @@ cons (name, (fixes, case_result c ctxt)); val cases = fold add_case (cases_of ctxt) []; in - if null cases andalso not (! verbose) then [] + if null cases then [] else [Pretty.big_list "cases:" (map pretty_case cases)] end; @@ -1310,6 +1299,8 @@ (* core context *) +val debug = Unsynchronized.ref false; +val verbose = Unsynchronized.ref false; val prems_limit = Unsynchronized.ref ~1; fun pretty_ctxt ctxt = @@ -1320,7 +1311,8 @@ (*structures*) val structs = Local_Syntax.structs_of (syntax_of ctxt); - val prt_structs = if null structs then [] + val prt_structs = + if null structs then [] else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: Pretty.commas (map Pretty.str structs))]; @@ -1331,7 +1323,8 @@ val fixes = rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1) (Variable.fixes_of ctxt)); - val prt_fixes = if null fixes then [] + val prt_fixes = + if null fixes then [] else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: Pretty.commas (map prt_fix fixes))]; @@ -1339,7 +1332,8 @@ val prems = Assumption.all_prems_of ctxt; val len = length prems; val suppressed = len - ! prems_limit; - val prt_prems = if null prems then [] + val prt_prems = + if null prems then [] else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @ map (Display.pretty_thm ctxt) (drop suppressed prems))]; in prt_structs @ prt_fixes @ prt_prems end; @@ -1349,6 +1343,9 @@ fun pretty_context ctxt = let + val is_verbose = ! verbose; + fun verb f x = if is_verbose then f (x ()) else []; + val prt_term = Syntax.pretty_term ctxt; val prt_typ = Syntax.pretty_typ ctxt; val prt_sort = Syntax.pretty_sort ctxt; diff -r 52ab455915d8 -r 3011b2149089 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Tue Feb 16 20:42:44 2010 +0100 @@ -123,9 +123,11 @@ val _ = inline "const" (Args.context -- Scan.lift Args.name_source -- Scan.optional (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] - >> (fn ((ctxt, c), Ts) => - let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c) - in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end)); + >> (fn ((ctxt, raw_c), Ts) => + let + val Const (c, _) = ProofContext.read_const_proper ctxt raw_c; + val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts)); + in ML_Syntax.atomic (ML_Syntax.print_term const) end)); val _ = inline "syntax_const" (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) => diff -r 52ab455915d8 -r 3011b2149089 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Tue Feb 16 20:42:44 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 52ab455915d8 -r 3011b2149089 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Feb 16 16:20:46 2010 +0100 +++ b/src/Pure/pure_thy.ML Tue Feb 16 20:42:44 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'(_')))"),