1.1 --- a/src/Pure/Isar/locale.ML Fri Dec 21 00:38:04 2001 +0100
1.2 +++ b/src/Pure/Isar/locale.ML Fri Dec 21 00:40:16 2001 +0100
1.3 @@ -1,6 +1,6 @@
1.4 (* Title: Pure/Isar/locale.ML
1.5 ID: $Id$
1.6 - Author: Markus Wenzel, TU München
1.7 + Author: Markus Wenzel, LMU München
1.8 License: GPL (GNU GENERAL PUBLIC LICENSE)
1.9
1.10 Locales -- Isar proof contexts as meta-level predicates, with local
1.11 @@ -53,7 +53,6 @@
1.12 structure Locale: LOCALE =
1.13 struct
1.14
1.15 -
1.16 (** locale elements and expressions **)
1.17
1.18 type context = ProofContext.context;
1.19 @@ -214,15 +213,16 @@
1.20 | inst_thm env th =
1.21 let
1.22 val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
1.23 - val cert = Thm.cterm_of sign and certT = Thm.ctyp_of sign;
1.24 - val names = foldr Term.add_term_tfree_names (prop :: hyps, []);
1.25 - val env' = filter (fn ((a, _), _) => a mem_string names) env;
1.26 + val cert = Thm.cterm_of sign;
1.27 + val certT = Thm.ctyp_of sign;
1.28 + val occs = foldr Term.add_term_tfree_names (prop :: hyps, []);
1.29 + val env' = filter (fn ((a, _), _) => a mem_string occs) env;
1.30 in
1.31 if null env' then th
1.32 else
1.33 th
1.34 |> Drule.implies_intr_list (map cert hyps)
1.35 - |> Drule.tvars_intr_list names
1.36 + |> Drule.tvars_intr_list (map (#1 o #1) env')
1.37 |> (fn (th', al) => th' |>
1.38 Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), []))
1.39 |> (fn th'' => Drule.implies_elim_list th''
1.40 @@ -324,7 +324,7 @@
1.41 ((name, map (apsnd (apsome (inst_type env))) ps), map (inst_elem env) elems);
1.42 in map inst (elemss ~~ envs) end;
1.43
1.44 -fun flatten_expr ctxt expr =
1.45 +fun flatten_expr ctxt (prev_idents, expr) =
1.46 let
1.47 val thy = ProofContext.theory_of ctxt;
1.48
1.49 @@ -370,22 +370,19 @@
1.50 val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems';
1.51 in ((name, params'), elems'') end;
1.52
1.53 - val raw_elemss = unique_parms ctxt (map eval (#1 (identify (([], []), expr))));
1.54 + val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
1.55 + val raw_elemss = unique_parms ctxt (map eval idents);
1.56 val elemss = unify_elemss ctxt [] raw_elemss;
1.57 - in elemss end;
1.58 + in (prev_idents @ idents, elemss) end;
1.59
1.60 end;
1.61
1.62
1.63 (* activate elements *)
1.64
1.65 -fun declare_fixes fixes =
1.66 - ProofContext.add_syntax fixes o
1.67 - ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes);
1.68 -
1.69 local
1.70
1.71 -fun activate_elem (Fixes fixes) = declare_fixes fixes
1.72 +fun activate_elem (Fixes fixes) = ProofContext.add_fixes fixes
1.73 | activate_elem (Assumes asms) =
1.74 #1 o ProofContext.assume_i ProofContext.export_assume asms o
1.75 ProofContext.fix_frees (flat (map (map #1 o #2) asms))
1.76 @@ -457,12 +454,12 @@
1.77 local
1.78
1.79 fun declare_int_elem i (ctxt, Fixes fixes) =
1.80 - (ctxt |> declare_fixes (map (fn (x, T, mx) =>
1.81 + (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
1.82 (x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), [])
1.83 | declare_int_elem _ (ctxt, _) = (ctxt, []);
1.84
1.85 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
1.86 - (ctxt |> declare_fixes (prep_fixes ctxt fixes), [])
1.87 + (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])
1.88 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
1.89 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
1.90 | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
1.91 @@ -480,10 +477,14 @@
1.92 let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t)))
1.93 in Term.list_all_free (frees, t) end;
1.94
1.95 +fun no_binds _ [] = []
1.96 + | no_binds ctxt _ = raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
1.97 +
1.98 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
1.99 - (a, map (fn (t, _) => (close_frees ctxt t, ([], []))) propps)))
1.100 - | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, _)) =>
1.101 - (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), []))))
1.102 + (a, map (fn (t, (ps, qs)) => (close_frees ctxt t,
1.103 + (no_binds ctxt ps, no_binds ctxt qs))) propps)))
1.104 + | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
1.105 + (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), no_binds ctxt ps))))
1.106 | closeup ctxt elem = elem;
1.107
1.108 fun finish_elem parms _ (Fixes fixes, _) = Ext (Fixes (map (fn (x, _, mx) =>
1.109 @@ -571,13 +572,16 @@
1.110 close fixed_params import elements raw_concl context =
1.111 let
1.112 val sign = ProofContext.sign_of context;
1.113 - fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]
1.114 - | flatten (Elem elem) = [(("", []), Ext elem)]
1.115 - | flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr));
1.116 + fun flatten (ids, Elem (Fixes fixes)) =
1.117 + (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
1.118 + | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
1.119 + | flatten (ids, Expr expr) =
1.120 + let val (ids', elemss) = flatten_expr context (ids, prep_expr sign expr)
1.121 + in (ids', map (apsnd Int) elemss) end
1.122 val activate = activate_facts prep_facts;
1.123
1.124 - val raw_import_elemss = flatten (Expr import);
1.125 - val raw_elemss = flat (map flatten elements);
1.126 + val (import_ids, raw_import_elemss) = flatten ([], Expr import);
1.127 + val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
1.128 val (parms, all_elemss, concl) =
1.129 prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
1.130
1.131 @@ -625,7 +629,7 @@
1.132
1.133 fun prt_syn syn =
1.134 let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
1.135 - in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
1.136 + in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
1.137 fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
1.138 prt_typ T :: Pretty.brk 1 :: prt_syn syn)
1.139 | prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);