1.1 --- a/src/Pure/Isar/proof_context.ML Tue May 31 11:53:37 2005 +0200
1.2 +++ b/src/Pure/Isar/proof_context.ML Tue May 31 11:53:38 2005 +0200
1.3 @@ -93,32 +93,22 @@
1.4 val get_thms_closure: context -> thmref -> thm list
1.5 val valid_thms: context -> string * thm list -> bool
1.6 val lthms_containing: context -> FactIndex.spec -> (string * thm list) list
1.7 - val cond_extern: context -> string -> xstring
1.8 - val qualified: bool -> context -> context
1.9 - val restore_qualified: context -> context -> context
1.10 + val extern: context -> string -> xstring
1.11 + val qualified_names: context -> context
1.12 + val no_base_names: context -> context
1.13 + val custom_accesses: (string list -> string list list) -> context -> context
1.14 + val restore_naming: context -> context -> context
1.15 val hide_thms: bool -> string list -> context -> context
1.16 val put_thm: string * thm -> context -> context
1.17 val put_thms: string * thm list -> context -> context
1.18 val put_thmss: (string * thm list) list -> context -> context
1.19 val reset_thms: string -> context -> context
1.20 val note_thmss:
1.21 - ((bstring * context attribute list) *
1.22 - (thmref * context attribute list) list) list ->
1.23 - context -> context * (bstring * thm list) list
1.24 + ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
1.25 + context -> context * (bstring * thm list) list
1.26 val note_thmss_i:
1.27 - ((bstring * context attribute list) *
1.28 - (thm list * context attribute list) list) list ->
1.29 - context -> context * (bstring * thm list) list
1.30 - val note_thmss_accesses:
1.31 - (string -> string list) ->
1.32 - ((bstring * context attribute list) *
1.33 - (thmref * context attribute list) list) list ->
1.34 - context -> context * (bstring * thm list) list
1.35 - val note_thmss_accesses_i:
1.36 - (string -> string list) ->
1.37 - ((bstring * context attribute list) *
1.38 - (thm list * context attribute list) list) list ->
1.39 - context -> context * (bstring * thm list) list
1.40 + ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
1.41 + context -> context * (bstring * thm list) list
1.42 val export_assume: exporter
1.43 val export_presume: exporter
1.44 val cert_def: context -> term -> string * term
1.45 @@ -143,10 +133,10 @@
1.46 val add_fixes_liberal: (string * typ option * Syntax.mixfix option) list -> context -> context
1.47 val fix_frees: term list -> context -> context
1.48 val bind_skolem: context -> string list -> term -> term
1.49 - val get_case: context -> string -> string option list -> RuleCases.T
1.50 - val add_cases: (string * RuleCases.T) list -> context -> context
1.51 val apply_case: RuleCases.T -> context
1.52 -> context * ((indexname * term option) list * (string * term list) list)
1.53 + val get_case: context -> string -> string option list -> RuleCases.T
1.54 + val add_cases: (string * RuleCases.T option) list -> context -> context
1.55 val verbose: bool ref
1.56 val setmp_verbose: ('a -> 'b) -> 'a -> 'b
1.57 val print_syntax: context -> unit
1.58 @@ -186,9 +176,8 @@
1.59 (string * thm list) list) * (*prems: A |- A *)
1.60 (string * string) list, (*fixes: !!x. _*)
1.61 binds: (term * typ) Vartab.table, (*term bindings*)
1.62 - thms: bool * NameSpace.T * thm list Symtab.table * FactIndex.T, (*local thms*)
1.63 - (*the bool indicates whether theorems with qualified names may be stored,
1.64 - cf. 'qualified' and 'restore_qualified'*)
1.65 + thms: NameSpace.naming * NameSpace.T *
1.66 + thm list Symtab.table * FactIndex.T, (*local thms*)
1.67 cases: (string * RuleCases.T) list, (*local contexts*)
1.68 defs:
1.69 typ Vartab.table * (*type constraints*)
1.70 @@ -314,7 +303,7 @@
1.71 fun init thy =
1.72 let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
1.73 make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
1.74 - (false, NameSpace.empty, Symtab.empty, FactIndex.empty), [],
1.75 + (NameSpace.default_naming, NameSpace.empty, Symtab.empty, FactIndex.empty), [],
1.76 (Vartab.empty, Vartab.empty, [], Symtab.empty))
1.77 end;
1.78
1.79 @@ -1004,7 +993,7 @@
1.80 fun valid_thms ctxt (name, ths) =
1.81 (case try (transform_error (fn () => get_thms ctxt (name, NONE))) () of
1.82 NONE => false
1.83 - | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
1.84 + | SOME ths' => Thm.eq_thms (ths, ths'));
1.85
1.86
1.87 (* lthms_containing *)
1.88 @@ -1017,37 +1006,37 @@
1.89
1.90 (* name space operations *)
1.91
1.92 -fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
1.93 +fun extern (Context {thms = (_, space, _, _), ...}) = NameSpace.extern space;
1.94
1.95 -fun qualified q = map_context (fn (thy, syntax, data, asms, binds,
1.96 - (_, space, tab, index), cases, defs) =>
1.97 - (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs));
1.98 +fun map_naming f = map_context (fn (thy, syntax, data, asms, binds,
1.99 + (naming, space, tab, index), cases, defs) =>
1.100 + (thy, syntax, data, asms, binds, (f naming, space, tab, index), cases, defs));
1.101
1.102 -fun restore_qualified (Context {thms, ...}) = qualified (#1 thms);
1.103 +val qualified_names = map_naming NameSpace.qualified_names;
1.104 +val no_base_names = map_naming NameSpace.no_base_names;
1.105 +val custom_accesses = map_naming o NameSpace.custom_accesses;
1.106 +fun restore_naming (Context {thms, ...}) = map_naming (K (#1 thms));
1.107
1.108 fun hide_thms fully names =
1.109 - map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
1.110 - (thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index),
1.111 - cases, defs));
1.112 + map_context (fn (thy, syntax, data, asms, binds, (naming, space, tab, index), cases, defs) =>
1.113 + (thy, syntax, data, asms, binds,
1.114 + (naming, fold (NameSpace.hide fully) names space, tab, index), cases, defs));
1.115
1.116
1.117 (* put_thm(s) *)
1.118
1.119 -fun gen_put_thms _ _ ("", _) ctxt = ctxt
1.120 - | gen_put_thms override_q acc (name, ths) ctxt = ctxt |> map_context
1.121 - (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
1.122 - if not override_q andalso not q andalso NameSpace.is_qualified name then
1.123 - raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
1.124 - else (thy, syntax, data, asms, binds, (q, NameSpace.extend' acc (space, [name]),
1.125 - Symtab.update ((name, ths), tab), FactIndex.add (is_known ctxt) (name, ths) index),
1.126 - cases, defs));
1.127 +fun put_thms ("", _) ctxt = ctxt
1.128 + | put_thms (bname, ths) ctxt = ctxt |> map_context
1.129 + (fn (thy, syntax, data, asms, binds, (naming, space, tab, index), cases, defs) =>
1.130 + let
1.131 + val name = NameSpace.full naming bname;
1.132 + val space' = NameSpace.declare naming name space;
1.133 + val tab' = Symtab.update ((name, ths), tab);
1.134 + val index' = FactIndex.add (is_known ctxt) (name, ths) index;
1.135 + in (thy, syntax, data, asms, binds, (naming, space', tab', index'), cases, defs) end);
1.136
1.137 -fun gen_put_thm q acc (name, th) = gen_put_thms q acc (name, [th]);
1.138 -fun gen_put_thmss q acc = fold (gen_put_thms q acc);
1.139 -
1.140 -val put_thm = gen_put_thm false NameSpace.accesses;
1.141 -val put_thms = gen_put_thms false NameSpace.accesses;
1.142 -val put_thmss = gen_put_thmss false NameSpace.accesses;
1.143 +fun put_thm (name, th) = put_thms (name, [th]);
1.144 +val put_thmss = fold put_thms;
1.145
1.146
1.147 (* reset_thms *)
1.148 @@ -1061,23 +1050,23 @@
1.149 (* note_thmss *)
1.150
1.151 local
1.152 -(* FIXME foldl_map (!?) *)
1.153 -fun gen_note_thss get acc (ctxt, ((name, more_attrs), ths_attrs)) =
1.154 +
1.155 +fun gen_note_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
1.156 let
1.157 fun app ((ct, ths), (th, attrs)) =
1.158 let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
1.159 in (ct', th' :: ths) end;
1.160 val (ctxt', rev_thms) = Library.foldl app ((ctxt, []), ths_attrs);
1.161 val thms = List.concat (rev rev_thms);
1.162 - in (ctxt' |> gen_put_thms true acc (name, thms), (name, thms)) end;
1.163 + in (ctxt' |> put_thms (name, thms), (name, thms)) end;
1.164
1.165 -fun gen_note_thmss get acc args ctxt =
1.166 - foldl_map (gen_note_thss get acc) (ctxt, args);
1.167 +fun gen_note_thmss get args ctxt =
1.168 + foldl_map (gen_note_thss get) (ctxt, args);
1.169
1.170 in
1.171
1.172 -val note_thmss = gen_note_thmss get_thms NameSpace.accesses;
1.173 -val note_thmss_i = gen_note_thmss (K I) NameSpace.accesses;
1.174 +val note_thmss = gen_note_thmss get_thms;
1.175 +val note_thmss_i = gen_note_thmss (K I);
1.176
1.177 val note_thmss_accesses = gen_note_thmss get_thms;
1.178 val note_thmss_accesses_i = gen_note_thmss (K I);
1.179 @@ -1282,6 +1271,15 @@
1.180
1.181 (** cases **)
1.182
1.183 +fun apply_case ({fixes, assumes, binds}: RuleCases.T) ctxt =
1.184 + let
1.185 + fun bind (c, (x, T)) = (c |> fix_i [([x], SOME T)], bind_skolem c [x] (Free (x, T)));
1.186 + val (ctxt', xs) = foldl_map bind (ctxt, fixes);
1.187 + fun app t = Library.foldl Term.betapply (t, xs);
1.188 + in (ctxt', (map (apsnd (Option.map app)) binds, map (apsnd (map app)) assumes)) end;
1.189 +
1.190 +local
1.191 +
1.192 fun prep_case ctxt name xs {fixes, assumes, binds} =
1.193 let
1.194 fun replace (opt_x :: xs) ((y, T) :: ys) = (if_none opt_x y, T) :: replace xs ys
1.195 @@ -1294,14 +1292,23 @@
1.196 else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
1.197 end;
1.198
1.199 +fun rem_case name = remove (fn (x, (y, _)) => x = y) name;
1.200 +
1.201 +fun add_case ("", _) cases = cases
1.202 + | add_case (name, NONE) cases = rem_case name cases
1.203 + | add_case (name, SOME c) cases = (name, c) :: rem_case name cases;
1.204 +
1.205 +in
1.206 +
1.207 fun get_case (ctxt as Context {cases, ...}) name xs =
1.208 (case assoc (cases, name) of
1.209 NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
1.210 | SOME c => prep_case ctxt name xs c);
1.211
1.212 +fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
1.213 + (thy, syntax, data, asms, binds, thms, fold add_case xs cases, defs));
1.214
1.215 -fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
1.216 - (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs));
1.217 +end;
1.218
1.219
1.220
1.221 @@ -1344,20 +1351,13 @@
1.222 (* local theorems *)
1.223
1.224 fun pretty_lthms (ctxt as Context {thms = (_, space, tab, _), ...}) =
1.225 - pretty_items (pretty_thm ctxt) "facts:" (NameSpace.cond_extern_table space tab);
1.226 + pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table space tab);
1.227
1.228 val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;
1.229
1.230
1.231 (* local contexts *)
1.232
1.233 -fun apply_case ({fixes, assumes, binds}: RuleCases.T) ctxt =
1.234 - let
1.235 - fun bind (c, (x, T)) = (c |> fix_i [([x], SOME T)], bind_skolem c [x] (Free (x, T)));
1.236 - val (ctxt', xs) = foldl_map bind (ctxt, fixes);
1.237 - fun app t = Library.foldl Term.betapply (t, xs);
1.238 - in (ctxt', (map (apsnd (Option.map app)) binds, map (apsnd (map app)) assumes)) end;
1.239 -
1.240 fun pretty_cases (ctxt as Context {cases, ...}) =
1.241 let
1.242 val prt_term = pretty_term ctxt;
1.243 @@ -1380,12 +1380,10 @@
1.244 (List.mapPartial (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
1.245 (if forall (null o #2) asms then []
1.246 else prt_sect "assume" [Pretty.str "and"] prt_asm asms)));
1.247 -
1.248 - val cases' = rev (Library.gen_distinct Library.eq_fst cases);
1.249 in
1.250 if null cases andalso not (! verbose) then []
1.251 else [Pretty.big_list "cases:"
1.252 - (map (prt_case o apsnd (fn c => (#fixes c, #2 (apply_case c ctxt)))) cases')]
1.253 + (map (prt_case o apsnd (fn c => (#fixes c, #2 (apply_case c ctxt)))) (rev cases))]
1.254 end;
1.255
1.256 val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;