refined notion of consts within the local scope;
authorwenzelm
Wed Nov 07 16:42:57 2007 +0100 (2007-11-07)
changeset 253250659c05cc107
parent 25324 ed4ac5966c68
child 25326 e417a7236125
refined notion of consts within the local scope;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Wed Nov 07 16:42:56 2007 +0100
     1.2 +++ b/src/Pure/variable.ML	Wed Nov 07 16:42:57 2007 +0100
     1.3 @@ -31,8 +31,9 @@
     1.4    val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
     1.5    val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
     1.6    val expand_binds: Proof.context -> term -> term
     1.7 +  val lookup_const: Proof.context -> string -> string option
     1.8    val is_const: Proof.context -> string -> bool
     1.9 -  val declare_const: string -> Proof.context -> Proof.context
    1.10 +  val declare_const: string * string -> Proof.context -> Proof.context
    1.11    val add_fixes: string list -> Proof.context -> string list * Proof.context
    1.12    val add_fixes_direct: string list -> Proof.context -> Proof.context
    1.13    val auto_fixes: term -> Proof.context -> Proof.context
    1.14 @@ -70,7 +71,7 @@
    1.15  datatype data = Data of
    1.16   {is_body: bool,                        (*inner body mode*)
    1.17    names: Name.context,                  (*type/term variable names*)
    1.18 -  scope: bool Symtab.table,             (*local scope of fixes/consts*)
    1.19 +  consts: string Symtab.table,          (*consts within the local scope*)
    1.20    fixes: (string * string) list,        (*term fixes -- extern/intern*)
    1.21    binds: (typ * term) Vartab.table,     (*term bindings*)
    1.22    type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
    1.23 @@ -79,8 +80,8 @@
    1.24      typ Vartab.table *                  (*type constraints*)
    1.25      sort Vartab.table};                 (*default sorts*)
    1.26  
    1.27 -fun make_data (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =
    1.28 -  Data {is_body = is_body, names = names, scope = scope, fixes = fixes, binds = binds,
    1.29 +fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =
    1.30 +  Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds,
    1.31      type_occs = type_occs, maxidx = maxidx, constraints = constraints};
    1.32  
    1.33  structure Data = ProofDataFun
    1.34 @@ -92,43 +93,43 @@
    1.35  );
    1.36  
    1.37  fun map_data f =
    1.38 -  Data.map (fn Data {is_body, names, scope, fixes, binds, type_occs, maxidx, constraints} =>
    1.39 -    make_data (f (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints)));
    1.40 +  Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, constraints} =>
    1.41 +    make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints)));
    1.42  
    1.43  fun map_names f =
    1.44 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.45 -    (is_body, f names, scope, fixes, binds, type_occs, maxidx, constraints));
    1.46 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.47 +    (is_body, f names, consts, fixes, binds, type_occs, maxidx, constraints));
    1.48  
    1.49 -fun map_scope f =
    1.50 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.51 -    (is_body, names, f scope, fixes, binds, type_occs, maxidx, constraints));
    1.52 +fun map_consts f =
    1.53 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.54 +    (is_body, names, f consts, fixes, binds, type_occs, maxidx, constraints));
    1.55  
    1.56  fun map_fixes f =
    1.57 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.58 -    (is_body, names, scope, f fixes, binds, type_occs, maxidx, constraints));
    1.59 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.60 +    (is_body, names, consts, f fixes, binds, type_occs, maxidx, constraints));
    1.61  
    1.62  fun map_binds f =
    1.63 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.64 -    (is_body, names, scope, fixes, f binds, type_occs, maxidx, constraints));
    1.65 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.66 +    (is_body, names, consts, fixes, f binds, type_occs, maxidx, constraints));
    1.67  
    1.68  fun map_type_occs f =
    1.69 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.70 -    (is_body, names, scope, fixes, binds, f type_occs, maxidx, constraints));
    1.71 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.72 +    (is_body, names, consts, fixes, binds, f type_occs, maxidx, constraints));
    1.73  
    1.74  fun map_maxidx f =
    1.75 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.76 -    (is_body, names, scope, fixes, binds, type_occs, f maxidx, constraints));
    1.77 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.78 +    (is_body, names, consts, fixes, binds, type_occs, f maxidx, constraints));
    1.79  
    1.80  fun map_constraints f =
    1.81 -  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.82 -    (is_body, names, scope, fixes, binds, type_occs, maxidx, f constraints));
    1.83 +  map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.84 +    (is_body, names, consts, fixes, binds, type_occs, maxidx, f constraints));
    1.85  
    1.86  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    1.87  
    1.88  val is_body = #is_body o rep_data;
    1.89  
    1.90 -fun set_body b = map_data (fn (_, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.91 -  (b, names, scope, fixes, binds, type_occs, maxidx, constraints));
    1.92 +fun set_body b = map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, constraints) =>
    1.93 +  (b, names, consts, fixes, binds, type_occs, maxidx, constraints));
    1.94  
    1.95  fun restore_body ctxt = set_body (is_body ctxt);
    1.96  
    1.97 @@ -255,12 +256,13 @@
    1.98  
    1.99  
   1.100  
   1.101 -(** local scope **)
   1.102 +(** consts **)
   1.103  
   1.104 -fun is_const ctxt x = the_default false (Symtab.lookup (#scope (rep_data ctxt)) x);
   1.105 +val lookup_const = Symtab.lookup o #consts o rep_data;
   1.106 +val is_const = is_some oo lookup_const;
   1.107  
   1.108 -fun declare_fixed x = map_scope (Symtab.update (x, false));
   1.109 -fun declare_const c = map_scope (Symtab.update (c, true));
   1.110 +val declare_fixed = map_consts o Symtab.delete_safe;
   1.111 +val declare_const = map_consts o Symtab.update;
   1.112  
   1.113  
   1.114