# HG changeset patch # User wenzelm # Date 1194450177 -3600 # Node ID 0659c05cc107f96430305b541e71ec4380975771 # Parent ed4ac5966c683522474980d3c616952401c6dbbe refined notion of consts within the local scope; diff -r ed4ac5966c68 -r 0659c05cc107 src/Pure/variable.ML --- a/src/Pure/variable.ML Wed Nov 07 16:42:56 2007 +0100 +++ b/src/Pure/variable.ML Wed Nov 07 16:42:57 2007 +0100 @@ -31,8 +31,9 @@ val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val add_binds: (indexname * term option) list -> Proof.context -> Proof.context val expand_binds: Proof.context -> term -> term + val lookup_const: Proof.context -> string -> string option val is_const: Proof.context -> string -> bool - val declare_const: string -> Proof.context -> Proof.context + val declare_const: string * string -> Proof.context -> Proof.context val add_fixes: string list -> Proof.context -> string list * Proof.context val add_fixes_direct: string list -> Proof.context -> Proof.context val auto_fixes: term -> Proof.context -> Proof.context @@ -70,7 +71,7 @@ datatype data = Data of {is_body: bool, (*inner body mode*) names: Name.context, (*type/term variable names*) - scope: bool Symtab.table, (*local scope of fixes/consts*) + consts: string Symtab.table, (*consts within the local scope*) fixes: (string * string) list, (*term fixes -- extern/intern*) binds: (typ * term) Vartab.table, (*term bindings*) type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) @@ -79,8 +80,8 @@ typ Vartab.table * (*type constraints*) sort Vartab.table}; (*default sorts*) -fun make_data (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) = - Data {is_body = is_body, names = names, scope = scope, fixes = fixes, binds = binds, +fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) = + Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds, type_occs = type_occs, maxidx = maxidx, constraints = constraints}; structure Data = ProofDataFun @@ -92,43 +93,43 @@ ); fun map_data f = - Data.map (fn Data {is_body, names, scope, fixes, binds, type_occs, maxidx, constraints} => - make_data (f (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints))); + Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, constraints} => + make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints))); fun map_names f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, f names, scope, fixes, binds, type_occs, maxidx, constraints)); + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, f names, consts, fixes, binds, type_occs, maxidx, constraints)); -fun map_scope f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, names, f scope, fixes, binds, type_occs, maxidx, constraints)); +fun map_consts f = + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, names, f consts, fixes, binds, type_occs, maxidx, constraints)); fun map_fixes f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, names, scope, f fixes, binds, type_occs, maxidx, constraints)); + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, names, consts, f fixes, binds, type_occs, maxidx, constraints)); fun map_binds f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, names, scope, fixes, f binds, type_occs, maxidx, constraints)); + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, names, consts, fixes, f binds, type_occs, maxidx, constraints)); fun map_type_occs f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, names, scope, fixes, binds, f type_occs, maxidx, constraints)); + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, names, consts, fixes, binds, f type_occs, maxidx, constraints)); fun map_maxidx f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, names, scope, fixes, binds, type_occs, f maxidx, constraints)); + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, names, consts, fixes, binds, type_occs, f maxidx, constraints)); fun map_constraints f = - map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (is_body, names, scope, fixes, binds, type_occs, maxidx, f constraints)); + map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (is_body, names, consts, fixes, binds, type_occs, maxidx, f constraints)); 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 (_, names, scope, fixes, binds, type_occs, maxidx, constraints) => - (b, names, scope, fixes, binds, type_occs, maxidx, constraints)); +fun set_body b = map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, constraints) => + (b, names, consts, fixes, binds, type_occs, maxidx, constraints)); fun restore_body ctxt = set_body (is_body ctxt); @@ -255,12 +256,13 @@ -(** local scope **) +(** consts **) -fun is_const ctxt x = the_default false (Symtab.lookup (#scope (rep_data ctxt)) x); +val lookup_const = Symtab.lookup o #consts o rep_data; +val is_const = is_some oo lookup_const; -fun declare_fixed x = map_scope (Symtab.update (x, false)); -fun declare_const c = map_scope (Symtab.update (c, true)); +val declare_fixed = map_consts o Symtab.delete_safe; +val declare_const = map_consts o Symtab.update;