--- a/src/Pure/Isar/locale.ML Fri Dec 21 00:38:04 2001 +0100
+++ b/src/Pure/Isar/locale.ML Fri Dec 21 00:40:16 2001 +0100
@@ -1,6 +1,6 @@
(* Title: Pure/Isar/locale.ML
ID: $Id$
- Author: Markus Wenzel, TU München
+ Author: Markus Wenzel, LMU München
License: GPL (GNU GENERAL PUBLIC LICENSE)
Locales -- Isar proof contexts as meta-level predicates, with local
@@ -53,7 +53,6 @@
structure Locale: LOCALE =
struct
-
(** locale elements and expressions **)
type context = ProofContext.context;
@@ -214,15 +213,16 @@
| inst_thm env th =
let
val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
- val cert = Thm.cterm_of sign and certT = Thm.ctyp_of sign;
- val names = foldr Term.add_term_tfree_names (prop :: hyps, []);
- val env' = filter (fn ((a, _), _) => a mem_string names) env;
+ val cert = Thm.cterm_of sign;
+ val certT = Thm.ctyp_of sign;
+ val occs = foldr Term.add_term_tfree_names (prop :: hyps, []);
+ val env' = filter (fn ((a, _), _) => a mem_string occs) env;
in
if null env' then th
else
th
|> Drule.implies_intr_list (map cert hyps)
- |> Drule.tvars_intr_list names
+ |> Drule.tvars_intr_list (map (#1 o #1) env')
|> (fn (th', al) => th' |>
Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), []))
|> (fn th'' => Drule.implies_elim_list th''
@@ -324,7 +324,7 @@
((name, map (apsnd (apsome (inst_type env))) ps), map (inst_elem env) elems);
in map inst (elemss ~~ envs) end;
-fun flatten_expr ctxt expr =
+fun flatten_expr ctxt (prev_idents, expr) =
let
val thy = ProofContext.theory_of ctxt;
@@ -370,22 +370,19 @@
val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems';
in ((name, params'), elems'') end;
- val raw_elemss = unique_parms ctxt (map eval (#1 (identify (([], []), expr))));
+ val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
+ val raw_elemss = unique_parms ctxt (map eval idents);
val elemss = unify_elemss ctxt [] raw_elemss;
- in elemss end;
+ in (prev_idents @ idents, elemss) end;
end;
(* activate elements *)
-fun declare_fixes fixes =
- ProofContext.add_syntax fixes o
- ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes);
-
local
-fun activate_elem (Fixes fixes) = declare_fixes fixes
+fun activate_elem (Fixes fixes) = ProofContext.add_fixes fixes
| activate_elem (Assumes asms) =
#1 o ProofContext.assume_i ProofContext.export_assume asms o
ProofContext.fix_frees (flat (map (map #1 o #2) asms))
@@ -457,12 +454,12 @@
local
fun declare_int_elem i (ctxt, Fixes fixes) =
- (ctxt |> declare_fixes (map (fn (x, T, mx) =>
+ (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
(x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), [])
| declare_int_elem _ (ctxt, _) = (ctxt, []);
fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
- (ctxt |> declare_fixes (prep_fixes ctxt fixes), [])
+ (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])
| declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
| declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
| declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
@@ -480,10 +477,14 @@
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t)))
in Term.list_all_free (frees, t) end;
+fun no_binds _ [] = []
+ | no_binds ctxt _ = raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
+
fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
- (a, map (fn (t, _) => (close_frees ctxt t, ([], []))) propps)))
- | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, _)) =>
- (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), []))))
+ (a, map (fn (t, (ps, qs)) => (close_frees ctxt t,
+ (no_binds ctxt ps, no_binds ctxt qs))) propps)))
+ | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
+ (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), no_binds ctxt ps))))
| closeup ctxt elem = elem;
fun finish_elem parms _ (Fixes fixes, _) = Ext (Fixes (map (fn (x, _, mx) =>
@@ -571,13 +572,16 @@
close fixed_params import elements raw_concl context =
let
val sign = ProofContext.sign_of context;
- fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]
- | flatten (Elem elem) = [(("", []), Ext elem)]
- | flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr));
+ fun flatten (ids, Elem (Fixes fixes)) =
+ (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
+ | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
+ | flatten (ids, Expr expr) =
+ let val (ids', elemss) = flatten_expr context (ids, prep_expr sign expr)
+ in (ids', map (apsnd Int) elemss) end
val activate = activate_facts prep_facts;
- val raw_import_elemss = flatten (Expr import);
- val raw_elemss = flat (map flatten elements);
+ val (import_ids, raw_import_elemss) = flatten ([], Expr import);
+ val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
val (parms, all_elemss, concl) =
prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
@@ -625,7 +629,7 @@
fun prt_syn syn =
let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
- in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
+ in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
prt_typ T :: Pretty.brk 1 :: prt_syn syn)
| prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);