# HG changeset patch # User wenzelm # Date 1152613029 -7200 # Node ID aa320957f00cfa360a159ae8868f4c700de1c35e # Parent 717b1eb434f18d9ee1f884c7e1a34ca78bdabd8f maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML); diff -r 717b1eb434f1 -r aa320957f00c src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Jul 11 12:17:08 2006 +0200 +++ b/src/Pure/variable.ML Tue Jul 11 12:17:09 2006 +0200 @@ -11,10 +11,9 @@ val set_body: bool -> Context.proof -> Context.proof val restore_body: Context.proof -> Context.proof -> Context.proof val fixes_of: Context.proof -> (string * string) list - val fixed_names_of: Context.proof -> string list val binds_of: Context.proof -> (typ * term) Vartab.table val defaults_of: Context.proof -> - typ Vartab.table * sort Vartab.table * string list * string list Symtab.table + typ Vartab.table * sort Vartab.table * string list * string list Symtab.table * Name.context val used_types: Context.proof -> string list val is_declared: Context.proof -> string -> bool val is_fixed: Context.proof -> string -> bool @@ -56,17 +55,19 @@ structure Variable: VARIABLE = struct + (** local context data **) datatype data = Data of - {is_body: bool, (*inner body mode*) - fixes: (string * string) list, (*term fixes -- extern/intern*) - binds: (typ * term) Vartab.table, (*term bindings*) + {is_body: bool, (*inner body mode*) + fixes: (string * string) list * Name.context, (*term fixes -- extern/intern*) + binds: (typ * term) Vartab.table, (*term bindings*) defaults: - typ Vartab.table * (*type constraints*) - sort Vartab.table * (*default sorts*) - string list * (*used type variables*) - string list Symtab.table}; (*occurrences of type variables in term variables*) + typ Vartab.table * (*type constraints*) + sort Vartab.table * (*default sorts*) + string list * (*used type variables*) + string list Symtab.table * (*occurrences of type variables in term variables*) + Name.context}; (*type/term variable names*) fun make_data (is_body, fixes, binds, defaults) = Data {is_body = is_body, fixes = fixes, binds = binds, defaults = defaults}; @@ -76,7 +77,8 @@ val name = "Pure/variable"; type T = data; fun init thy = - make_data (false, [], Vartab.empty, (Vartab.empty, Vartab.empty, [], Symtab.empty)); + make_data (false, ([], Name.context), Vartab.empty, + (Vartab.empty, Vartab.empty, [], Symtab.empty, Name.make_context ["", "'"])); fun print _ _ = (); ); @@ -98,11 +100,12 @@ fun rep_data ctxt = Data.get ctxt |> (fn Data args => args); val is_body = #is_body o rep_data; -fun set_body b = map_data (fn (_, fixes, binds, defaults) => (b, fixes, binds, defaults)); +fun set_body b = map_data (fn (_, fixes, binds, defaults) => + (b, fixes, binds, defaults)); fun restore_body ctxt = set_body (is_body ctxt); -val fixes_of = #fixes o rep_data; -val fixed_names_of = map #2 o fixes_of; +val fixes_of = #1 o #fixes o rep_data; +val fixed_names_of = #2 o #fixes o rep_data; val binds_of = #binds o rep_data; @@ -122,7 +125,7 @@ val def_sort = Vartab.lookup o #2 o defaults_of; fun def_type ctxt pattern xi = - let val {binds, defaults = (types, _, _, _), ...} = rep_data ctxt in + let val {binds, defaults = (types, _, _, _, _), ...} = rep_data ctxt in (case Vartab.lookup types xi of NONE => if pattern then NONE @@ -159,31 +162,41 @@ SOME T => Vartab.update ((x, ~1), T) | NONE => I)); +val ins_namesT = fold_atyps + (fn TFree (x, _) => Name.declare x | _ => I); + +fun ins_names t = + fold_types ins_namesT t #> + fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t; + in -fun declare_type T = map_defaults (fn (types, sorts, used, occ) => +fun declare_type T = map_defaults (fn (types, sorts, used, occ, names) => (types, ins_sorts T sorts, ins_used T used, - occ)); + occ, + ins_namesT T names)); -fun declare_syntax t = map_defaults (fn (types, sorts, used, occ) => +fun declare_syntax t = map_defaults (fn (types, sorts, used, occ, names) => (ins_types t types, fold_types ins_sorts t sorts, fold_types ins_used t used, - occ)); + occ, + ins_names t names)); -fun declare_occs t = map_defaults (fn (types, sorts, used, occ) => - (types, sorts, used, ins_occs t occ)); +fun declare_occs t = map_defaults (fn (types, sorts, used, occ, names) => + (types, sorts, used, ins_occs t occ, names)); fun declare_term t ctxt = ctxt |> declare_syntax t - |> map_defaults (fn (types, sorts, used, occ) => + |> map_defaults (fn (types, sorts, used, occ, names) => (ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types, sorts, used, - ins_occs t occ)); + ins_occs t occ, + ins_names t names)); fun declare_thm th = fold declare_term (Thm.full_prop_of th :: Thm.hyps_of th); fun thm_context th = Context.init_proof (Thm.theory_of_thm th) |> declare_thm th; @@ -195,48 +208,52 @@ fun rename_wrt ctxt ts frees = let - val (types, sorts, _, _) = defaults_of (ctxt |> fold declare_syntax ts); - fun ren (x, X) xs = - let - fun used y = y = "" orelse y = "'" orelse member (op =) xs y orelse - Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1); - val x' = Term.variant_name used x; - in ((x', X), x' :: xs) end; - in #1 (fold_map ren frees []) end; + val names = #5 (defaults_of (ctxt |> fold declare_syntax ts)); + val xs = fst (Name.variants (map #1 frees) names); + in xs ~~ map snd frees end; (** fixes **) +local + fun no_dups [] = () | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups); +fun new_fixes xs xs' names' = + map_fixes (fn (fixes, _) => (rev (xs ~~ xs') @ fixes, names')) #> + fold (declare_syntax o Syntax.free) xs' #> + pair xs'; + +in + fun add_fixes xs ctxt = let - val (ys, zs) = split_list (fixes_of ctxt); - val _ = no_dups (duplicates (op =) xs); val _ = - (case filter (can Term.dest_skolem) xs of [] => () + (case filter (can Name.dest_skolem) xs of [] => () | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads)); - val xs' = - if is_body ctxt then Term.variantlist (map Term.skolem xs, zs) - else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); xs); - in - ctxt - |> map_fixes (fn fixes => rev (xs ~~ xs') @ fixes) - |> fold (declare_syntax o Syntax.free) xs' - |> pair xs' - end; + val _ = no_dups (duplicates (op =) xs); + val (ys, zs) = split_list (fixes_of ctxt); + val names = fixed_names_of ctxt; + val (xs', names') = + if is_body ctxt then Name.variants (map Name.skolem xs) names + else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); + (xs, fold Name.declare xs names)); + in ctxt |> new_fixes xs xs' names' end; -fun invent_fixes xs ctxt = - ctxt - |> set_body true - |> add_fixes (Term.variantlist (xs, [])) - ||> restore_body ctxt; +fun invent_fixes raw_xs ctxt = + let + val names = fixed_names_of ctxt; + val (xs, names') = Name.variants (map Name.clean raw_xs) names; + val xs' = map Name.skolem xs; + in ctxt |> new_fixes xs xs' names' end; + +end; fun invent_types Ss ctxt = let - val tfrees = Term.invent_names (used_types ctxt) "'a" (length Ss) ~~ Ss; + val tfrees = Name.invents (#5 (defaults_of ctxt)) "'a" (length Ss) ~~ Ss; val ctxt' = fold (declare_type o TFree) tfrees ctxt; in (tfrees, ctxt') end; @@ -291,7 +308,7 @@ let val (instT, ctxt') = importT_inst ts ctxt; val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts [])); - val ren = if is_open then I else Term.internal; + val ren = if is_open then I else Name.internal; val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt'; val inst = vars ~~ map Free (xs ~~ map #2 vars); in ((instT, inst), ctxt'') end;