1.1 --- a/src/Pure/Isar/locale.ML Tue Aug 26 14:15:44 2008 +0200
1.2 +++ b/src/Pure/Isar/locale.ML Tue Aug 26 16:04:22 2008 +0200
1.3 @@ -207,6 +207,21 @@
1.4
1.5 (** management of registrations in theories and proof contexts **)
1.6
1.7 +type registration =
1.8 + {attn: (bool * string) * Attrib.src list,
1.9 + (* parameters and prefix
1.10 + (if the Boolean flag is set, only accesses containing the prefix are generated,
1.11 + otherwise the prefix may be omitted when accessing theorems etc.) *)
1.12 + exp: Morphism.morphism,
1.13 + (* maps content to its originating context *)
1.14 + imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
1.15 + (* inverse of exp *)
1.16 + wits: Element.witness list,
1.17 + (* witnesses of the registration *)
1.18 + eqns: thm Termtab.table
1.19 + (* theorems (equations) interpreting derived concepts and indexed by lhs *)
1.20 + }
1.21 +
1.22 structure Registrations :
1.23 sig
1.24 type T
1.25 @@ -225,26 +240,25 @@
1.26 Element.witness list *
1.27 thm Termtab.table) option
1.28 val insert: theory -> term list -> ((bool * string) * Attrib.src list) ->
1.29 - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> T ->
1.30 + (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
1.31 + T ->
1.32 T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
1.33 val add_witness: term list -> Element.witness -> T -> T
1.34 val add_equation: term list -> thm -> T -> T
1.35 end =
1.36 struct
1.37 - (* A registration is indexed by parameter instantiation. Its components are:
1.38 - - parameters and prefix
1.39 - (if the Boolean flag is set, only accesses containing the prefix are generated,
1.40 - otherwise the prefix may be omitted when accessing theorems etc.)
1.41 - - pair of export and import morphisms, export maps content to its originating
1.42 - context, import is its inverse
1.43 - - theorems (actually witnesses) instantiating locale assumptions
1.44 - - theorems (equations) interpreting derived concepts and indexed by lhs.
1.45 - NB: index is exported whereas content is internalised.
1.46 - *)
1.47 - type T = (((bool * string) * Attrib.src list) *
1.48 - (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
1.49 - Element.witness list *
1.50 - thm Termtab.table) Termtab.table;
1.51 + (* A registration is indexed by parameter instantiation.
1.52 + NB: index is exported whereas content is internalised. *)
1.53 + type T = registration Termtab.table;
1.54 +
1.55 + fun mk_reg attn exp imp wits eqns =
1.56 + {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns};
1.57 +
1.58 + fun map_reg f reg =
1.59 + let
1.60 + val {attn, exp, imp, wits, eqns} = reg;
1.61 + val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns);
1.62 + in mk_reg attn' exp' imp' wits' eqns' end;
1.63
1.64 val empty = Termtab.empty;
1.65
1.66 @@ -261,14 +275,15 @@
1.67 - witnesses are equal, no attempt to subsumption testing;
1.68 - union of equalities, if conflicting (i.e. two eqns with equal lhs)
1.69 eqn of right theory takes precedence *)
1.70 - fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, _, e1), (n, m, w, e2)) =>
1.71 - (n, m, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
1.72 + fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) =>
1.73 + mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
1.74
1.75 fun dest_transfer thy regs =
1.76 - Termtab.dest regs |> map (apsnd (fn (n, m, ws, es) =>
1.77 - (n, m, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es)));
1.78 -
1.79 - fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
1.80 + Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es) =>
1.81 + (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
1.82 +
1.83 + fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
1.84 + map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns)));
1.85
1.86 (* registrations that subsume t *)
1.87 fun subsumers thy t regs =
1.88 @@ -286,7 +301,7 @@
1.89 in
1.90 (case subs of
1.91 [] => NONE
1.92 - | ((t', ((prfx, atts), (exp', ((impT', domT'), (imp', dom'))), thms, eqns)) :: _) =>
1.93 + | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
1.94 let
1.95 val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
1.96 val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
1.97 @@ -297,14 +312,14 @@
1.98 |> var_inst_term (impT, imp))) |> Symtab.make;
1.99 val inst'_morph = Element.inst_morphism thy (tinst', inst');
1.100 in SOME ((prfx, map (Args.morph_values inst'_morph) atts),
1.101 - map (Element.morph_witness inst'_morph) thms,
1.102 + map (Element.morph_witness inst'_morph) wits,
1.103 Termtab.map (Morphism.thm inst'_morph) eqns)
1.104 end)
1.105 end;
1.106
1.107 (* add registration if not subsumed by ones already present,
1.108 additionally returns registrations that are strictly subsumed *)
1.109 - fun insert thy ts attn m regs =
1.110 + fun insert thy ts attn (exp, imp) regs =
1.111 let
1.112 val t = termify ts;
1.113 val subs = subsumers thy t regs ;
1.114 @@ -312,8 +327,8 @@
1.115 [] => let
1.116 val sups =
1.117 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
1.118 - val sups' = map (apfst untermify) sups |> map (fn (ts, (n, _, w, _)) => (ts, (n, w)))
1.119 - in (Termtab.update (t, (attn, m, [], Termtab.empty)) regs, sups') end
1.120 + val sups' = map (apfst untermify) sups |> map (fn (ts, {attn, wits, ...}) => (ts, (attn, wits)))
1.121 + in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end
1.122 | _ => (regs, []))
1.123 end;
1.124
1.125 @@ -321,21 +336,21 @@
1.126 let
1.127 val t = termify ts;
1.128 in
1.129 - Termtab.update (t, f (the (Termtab.lookup regs t))) regs
1.130 + Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
1.131 end;
1.132
1.133 (* add witness theorem to registration,
1.134 only if instantiation is exact, otherwise exception Option raised *)
1.135 fun add_witness ts wit regs =
1.136 - gen_add (fn (x, m, wits, eqns) => (x, m, Element.close_witness wit :: wits, eqns))
1.137 + gen_add (fn (x, e, i, wits, eqns) => (x, e, i, Element.close_witness wit :: wits, eqns))
1.138 ts regs;
1.139
1.140 (* add equation to registration, replaces previous equation with same lhs;
1.141 only if instantiation is exact, otherwise exception Option raised;
1.142 exception TERM raised if not a meta equality *)
1.143 fun add_equation ts thm regs =
1.144 - gen_add (fn (x, m, thms, eqns) =>
1.145 - (x, m, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns))
1.146 + gen_add (fn (x, e, i, thms, eqns) =>
1.147 + (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns))
1.148 ts regs;
1.149 end;
1.150
1.151 @@ -449,12 +464,12 @@
1.152
1.153 (* add registration to theory or context, ignored if subsumed *)
1.154
1.155 -fun put_registration (name, ps) attn morphs ctxt =
1.156 +fun put_registration (name, ps) attn morphs (* wits *) ctxt =
1.157 RegistrationsData.map (fn regs =>
1.158 let
1.159 val thy = Context.theory_of ctxt;
1.160 val reg = the_default Registrations.empty (Symtab.lookup regs name);
1.161 - val (reg', sups) = Registrations.insert thy ps attn morphs reg;
1.162 + val (reg', sups) = Registrations.insert thy ps attn morphs (* wits *) reg;
1.163 val _ = if not (null sups) then warning
1.164 ("Subsumed interpretation(s) of locale " ^
1.165 quote (extern thy name) ^
1.166 @@ -2044,45 +2059,46 @@
1.167 attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
1.168 let
1.169 val ctxt = mk_ctxt thy_ctxt;
1.170 - val (propss, eq_props) = chop (length all_elemss) propss;
1.171 - val (thmss, eq_thms) = chop (length all_elemss) thmss;
1.172 + val (all_propss, eq_props) = chop (length all_elemss) propss;
1.173 + val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
1.174
1.175 (* Filter out fragments already registered. *)
1.176
1.177 val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
1.178 - test_reg thy_ctxt id) (all_elemss ~~ (propss ~~ thmss)));
1.179 - val (propss, thmss) = split_list xs;
1.180 -
1.181 - fun activate_elem prems eqns exp loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
1.182 + test_reg thy_ctxt id) (all_elemss ~~ (all_propss ~~ all_thmss)));
1.183 + val (new_propss, new_thmss) = split_list xs;
1.184 +
1.185 + val thy_ctxt' = thy_ctxt
1.186 + (* add registrations *)
1.187 +(* |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *)
1.188 + |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss
1.189 + (* add witnesses of Assumed elements (only those generate proof obligations) *)
1.190 + |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
1.191 + (* add equations *)
1.192 + |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
1.193 + (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
1.194 + Element.conclude_witness) eq_thms);
1.195 +
1.196 + val prems = flat (map_filter
1.197 + (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
1.198 + | ((_, Derived _), _) => NONE) all_elemss);
1.199 +
1.200 + fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
1.201 let
1.202 val ctxt = mk_ctxt thy_ctxt;
1.203 val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
1.204 (Symtab.empty, Symtab.empty) prems eqns atts
1.205 exp (attrib thy_ctxt) facts;
1.206 in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
1.207 - | activate_elem _ _ _ _ _ _ thy_ctxt = thy_ctxt;
1.208 -
1.209 - fun activate_elems prems eqns exp ((id, _), elems) thy_ctxt =
1.210 + | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
1.211 +
1.212 + fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
1.213 let
1.214 val (prfx_atts, _, _) = case get_reg thy_ctxt imp id
1.215 of SOME x => x
1.216 | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
1.217 ^ " while activating facts.");
1.218 - in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp (fst id) prfx_atts) elems thy_ctxt end;
1.219 -
1.220 - val thy_ctxt' = thy_ctxt
1.221 - (* add registrations *)
1.222 - |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss
1.223 - (* add witnesses of Assumed elements (only those generate proof obligations) *)
1.224 - |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss)
1.225 - (* add equations *)
1.226 - |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
1.227 - (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
1.228 - Element.conclude_witness) eq_thms);
1.229 -
1.230 - val prems = flat (map_filter
1.231 - (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
1.232 - | ((_, Derived _), _) => NONE) all_elemss);
1.233 + in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end;
1.234
1.235 val thy_ctxt'' = thy_ctxt'
1.236 (* add witnesses of Derived elements *)
1.237 @@ -2092,7 +2108,7 @@
1.238
1.239 (* Accumulate equations *)
1.240 val all_eqns =
1.241 - fold_map (join_eqns (get_reg thy_ctxt'' imp) (fst o fst) ctxt) all_elemss Termtab.empty
1.242 + fold_map (join_eqns (get_reg thy_ctxt'' imp) fst ctxt) all_propss Termtab.empty
1.243 |> fst
1.244 |> map (apsnd (map snd o Termtab.dest))
1.245 |> (fn xs => fold Idtab.update xs Idtab.empty)
1.246 @@ -2108,7 +2124,7 @@
1.247 [([Element.conclude_witness thm], [])])] #> snd)
1.248 (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms)
1.249 (* add facts *)
1.250 - |> fold (activate_elems prems all_eqns exp) new_elemss
1.251 + |> fold (activate_elems all_eqns) new_elemss
1.252 end;
1.253
1.254 fun global_activate_facts_elemss x = gen_activate_facts_elemss