# HG changeset patch # User wenzelm # Date 1003943903 -7200 # Node ID 4747b4b8409366ff0a1f5e79c8e1dfcb7f87e508 # Parent b6def266cbb9b5bb88b2889a84949d53e255a63c added read_prop_schematic; diff -r b6def266cbb9 -r 4747b4b84093 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Oct 24 19:18:10 2001 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Oct 24 19:18:23 2001 +0200 @@ -28,6 +28,7 @@ val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list val read_term: context -> string -> term val read_prop: context -> string -> term + val read_prop_schematic: context -> string -> term val read_terms: context -> string list -> term list val read_termT_pats: context -> (string * typ) list -> term list val read_term_pats: typ -> context -> string list -> term list @@ -82,14 +83,15 @@ val export_def: exporter val assume: exporter -> ((string * context attribute list) * (string * (string list * string list)) list) list - -> context -> context * ((string * thm list) list * thm list) + -> context -> context * (string * thm list) list val assume_i: exporter -> ((string * context attribute list) * (term * (term list * term list)) list) list - -> context -> context * ((string * thm list) list * thm list) + -> context -> context * (string * thm list) list val read_vars: context * (string list * string option) -> context * (string list * typ option) val cert_vars: context * (string list * typ option) -> context * (string list * typ option) val fix: (string list * string option) list -> context -> context val fix_i: (string list * typ option) list -> context -> context + val fix_direct: (string list * typ option) list -> context -> context val bind_skolem: context -> string list -> term -> term val get_case: context -> string -> string option list -> RuleCases.T val add_cases: (string * RuleCases.T) list -> context -> context @@ -157,7 +159,6 @@ fun prems_of (Context {asms = ((_, asms), _), ...}) = flat (map #2 asms); - (** user data **) (* errors *) @@ -288,9 +289,9 @@ in -val read_typ = read_typ_aux Sign.read_typ; +val read_typ = read_typ_aux Sign.read_typ; val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm; -val cert_typ = cert_typ_aux Sign.certify_typ; +val cert_typ = cert_typ_aux Sign.certify_typ; val cert_typ_no_norm = cert_typ_aux Sign.certify_typ_no_norm; end; @@ -435,6 +436,7 @@ val read_term = gen_read (read_term_sg true) I false false; val read_prop = gen_read (read_prop_sg true) I false false; +val read_prop_schematic = gen_read (read_prop_sg true) I false true; val read_terms = gen_read (read_terms_sg true) map false false; val read_props = gen_read (read_props_sg true) map false; @@ -762,14 +764,14 @@ in -val read_propp = prep_propp false read_props read_prop_pats; -val cert_propp = prep_propp false cert_props cert_prop_pats; +val read_propp = prep_propp false read_props read_prop_pats; +val cert_propp = prep_propp false cert_props cert_prop_pats; val read_propp_schematic = prep_propp true read_props read_prop_pats; val cert_propp_schematic = prep_propp true cert_props cert_prop_pats; -val bind_propp = gen_bind_propp read_propp; -val bind_propp_i = gen_bind_propp cert_propp; -val bind_propp_schematic = gen_bind_propp read_propp_schematic; +val bind_propp = gen_bind_propp read_propp; +val bind_propp_i = gen_bind_propp cert_propp; +val bind_propp_schematic = gen_bind_propp read_propp_schematic; val bind_propp_schematic_i = gen_bind_propp cert_propp_schematic; end; @@ -886,7 +888,8 @@ |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => (thy, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, cases, defs)); - in (warn_extra_tfrees ctxt ctxt3, (thmss, prems_of ctxt3)) end; + val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3); + in (warn_extra_tfrees ctxt ctxt4, thmss) end; in @@ -900,9 +903,9 @@ local -fun prep_vars prep_typ (ctxt, (xs, raw_T)) = +fun prep_vars prep_typ no_internal (ctxt, (xs, raw_T)) = let - val _ = (case filter (not o Syntax.is_identifier) (map (no_skolem false ctxt) xs) of + val _ = (case filter (not o Syntax.is_identifier) (map (no_skolem no_internal ctxt) xs) of [] => () | bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt)); val opt_T = apsome (prep_typ ctxt) raw_T; @@ -912,8 +915,8 @@ in -val read_vars = prep_vars read_typ; -val cert_vars = prep_vars cert_typ; +val read_vars = prep_vars read_typ true; +val cert_vars = prep_vars cert_typ false; end; @@ -922,31 +925,37 @@ local -fun add_vars xs (fixes, names) = - let - val xs' = variantlist (xs, names); - val fixes' = (xs ~~ map Syntax.skolem xs') @ fixes; - val names' = xs' @ names; - in (fixes', names') end; - fun map_vars f = map_context (fn (thy, data, (assumes, vars), binds, thms, cases, defs) => (thy, data, (assumes, f vars), binds, thms, cases, defs)); -fun gen_fix prep raw_vars ctxt = +fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt); + +fun add_vars _ xs (fixes, used) = + let + val xs' = variantlist (xs, used); + val fixes' = (xs ~~ map Syntax.skolem xs') @ fixes; + val used' = xs' @ used; + in (fixes', used') end; + +fun add_vars_direct ctxt xs (fixes, used) = + (case xs inter_string map #1 fixes of + [] => ((xs ~~ xs) @ fixes, xs @ used) + | dups => err_dups ctxt dups); + +fun gen_fix prep add raw_vars ctxt = let val (ctxt', varss) = foldl_map prep (ctxt, raw_vars); val xs = flat (map fst varss); in - (case Library.duplicates xs of - [] => () - | dups => raise CONTEXT ("Duplicate variable name(s): " ^ commas_quote dups, ctxt)); - ctxt' |> map_vars (add_vars xs) + (case Library.duplicates xs of [] => () | dups => err_dups ctxt dups); + ctxt' |> map_vars (add ctxt xs) end; in -val fix = gen_fix read_vars; -val fix_i = gen_fix cert_vars; +val fix = gen_fix read_vars add_vars; +val fix_i = gen_fix cert_vars add_vars; +val fix_direct = gen_fix cert_vars add_vars_direct; end;