src/Pure/variable.ML
changeset 25316 17c183417f93
parent 25051 71cd45fdf332
child 25325 0659c05cc107
     1.1 --- a/src/Pure/variable.ML	Tue Nov 06 20:27:33 2007 +0100
     1.2 +++ b/src/Pure/variable.ML	Tue Nov 06 22:50:34 2007 +0100
     1.3 @@ -31,6 +31,8 @@
     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 is_const: Proof.context -> string -> bool
     1.8 +  val declare_const: string -> Proof.context -> Proof.context
     1.9    val add_fixes: string list -> Proof.context -> string list * Proof.context
    1.10    val add_fixes_direct: string list -> Proof.context -> Proof.context
    1.11    val auto_fixes: term -> Proof.context -> Proof.context
    1.12 @@ -68,6 +70,7 @@
    1.13  datatype data = Data of
    1.14   {is_body: bool,                        (*inner body mode*)
    1.15    names: Name.context,                  (*type/term variable names*)
    1.16 +  scope: bool Symtab.table,             (*local scope of fixes/consts*)
    1.17    fixes: (string * string) list,        (*term fixes -- extern/intern*)
    1.18    binds: (typ * term) Vartab.table,     (*term bindings*)
    1.19    type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
    1.20 @@ -76,46 +79,56 @@
    1.21      typ Vartab.table *                  (*type constraints*)
    1.22      sort Vartab.table};                 (*default sorts*)
    1.23  
    1.24 -fun make_data (is_body, names, fixes, binds, type_occs, maxidx, constraints) =
    1.25 -  Data {is_body = is_body, names = names, fixes = fixes, binds = binds,
    1.26 +fun make_data (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =
    1.27 +  Data {is_body = is_body, names = names, scope = scope, fixes = fixes, binds = binds,
    1.28      type_occs = type_occs, maxidx = maxidx, constraints = constraints};
    1.29  
    1.30  structure Data = ProofDataFun
    1.31  (
    1.32    type T = data;
    1.33    fun init thy =
    1.34 -    make_data (false, Name.context, [], Vartab.empty, Symtab.empty,
    1.35 +    make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty,
    1.36        ~1, (Vartab.empty, Vartab.empty));
    1.37  );
    1.38  
    1.39  fun map_data f =
    1.40 -  Data.map (fn Data {is_body, names, fixes, binds, type_occs, maxidx, constraints} =>
    1.41 -    make_data (f (is_body, names, fixes, binds, type_occs, maxidx, constraints)));
    1.42 +  Data.map (fn Data {is_body, names, scope, fixes, binds, type_occs, maxidx, constraints} =>
    1.43 +    make_data (f (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints)));
    1.44 +
    1.45 +fun map_names f =
    1.46 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.47 +    (is_body, f names, scope, fixes, binds, type_occs, maxidx, constraints));
    1.48  
    1.49 -fun map_names f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.50 -  (is_body, f names, fixes, binds, type_occs, maxidx, constraints));
    1.51 +fun map_scope f =
    1.52 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.53 +    (is_body, names, f scope, fixes, binds, type_occs, maxidx, constraints));
    1.54  
    1.55 -fun map_fixes f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.56 -  (is_body, names, f fixes, binds, type_occs, maxidx, constraints));
    1.57 +fun map_fixes f =
    1.58 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.59 +    (is_body, names, scope, f fixes, binds, type_occs, maxidx, constraints));
    1.60  
    1.61 -fun map_binds f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.62 -  (is_body, names, fixes, f binds, type_occs, maxidx, constraints));
    1.63 +fun map_binds f =
    1.64 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.65 +    (is_body, names, scope, fixes, f binds, type_occs, maxidx, constraints));
    1.66  
    1.67 -fun map_type_occs f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.68 -  (is_body, names, fixes, binds, f type_occs, maxidx, constraints));
    1.69 +fun map_type_occs f =
    1.70 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.71 +    (is_body, names, scope, fixes, binds, f type_occs, maxidx, constraints));
    1.72  
    1.73 -fun map_maxidx f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.74 -  (is_body, names, fixes, binds, type_occs, f maxidx, constraints));
    1.75 +fun map_maxidx f =
    1.76 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.77 +    (is_body, names, scope, fixes, binds, type_occs, f maxidx, constraints));
    1.78  
    1.79 -fun map_constraints f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.80 -  (is_body, names, fixes, binds, type_occs, maxidx, f constraints));
    1.81 +fun map_constraints f =
    1.82 +  map_data (fn (is_body, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.83 +    (is_body, names, scope, fixes, binds, type_occs, maxidx, f constraints));
    1.84  
    1.85  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    1.86  
    1.87  val is_body = #is_body o rep_data;
    1.88  
    1.89 -fun set_body b = map_data (fn (_, names, fixes, binds, type_occs, maxidx, constraints) =>
    1.90 -  (b, names, fixes, binds, type_occs, maxidx, constraints));
    1.91 +fun set_body b = map_data (fn (_, names, scope, fixes, binds, type_occs, maxidx, constraints) =>
    1.92 +  (b, names, scope, fixes, binds, type_occs, maxidx, constraints));
    1.93  
    1.94  fun restore_body ctxt = set_body (is_body ctxt);
    1.95  
    1.96 @@ -242,6 +255,15 @@
    1.97  
    1.98  
    1.99  
   1.100 +(** local scope **)
   1.101 +
   1.102 +fun is_const ctxt x = the_default false (Symtab.lookup (#scope (rep_data ctxt)) x);
   1.103 +
   1.104 +fun declare_fixed x = map_scope (Symtab.update (x, false));
   1.105 +fun declare_const c = map_scope (Symtab.update (c, true));
   1.106 +
   1.107 +
   1.108 +
   1.109  (** fixes **)
   1.110  
   1.111  local
   1.112 @@ -251,6 +273,7 @@
   1.113  
   1.114  fun new_fixes names' xs xs' =
   1.115    map_names (K names') #>
   1.116 +  fold declare_fixed xs #>
   1.117    map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #>
   1.118    fold (declare_constraints o Syntax.free) xs' #>
   1.119    pair xs';