--- 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;
--- 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
--- 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
--- 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\<lparr>_\<rparr>)")
"_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
"_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
- "_record_update" :: "'a => updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
+ "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
subsection {* Record package *}
--- 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
--- 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]);
--- 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);
--- 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. *)
--- 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 [("<unnamed>", 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;
--- 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) =>
--- 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')];
--- 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 "'\\<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'(_')))"),