src/Pure/Isar/locale.ML
changeset 28005 0e71a3b1b396
parent 27865 27a8ad9612a3
child 28020 1ff5167592ba
     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,37 +2059,21 @@
   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 -        let
   1.183 -          val ctxt = mk_ctxt thy_ctxt;
   1.184 -          val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
   1.185 -              (Symtab.empty, Symtab.empty) prems eqns atts
   1.186 -              exp (attrib thy_ctxt) facts;
   1.187 -        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
   1.188 -      | activate_elem _ _ _ _ _ _ thy_ctxt = thy_ctxt;
   1.189 -
   1.190 -    fun activate_elems prems eqns exp ((id, _), elems) thy_ctxt =
   1.191 -      let
   1.192 -        val (prfx_atts, _, _) = case get_reg thy_ctxt imp id
   1.193 -         of SOME x => x
   1.194 -          | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
   1.195 -              ^ " while activating facts.");
   1.196 -      in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp (fst id) prfx_atts) elems thy_ctxt end;
   1.197 +          test_reg thy_ctxt id) (all_elemss ~~ (all_propss ~~ all_thmss)));
   1.198 +    val (new_propss, new_thmss) = split_list xs;
   1.199  
   1.200      val thy_ctxt' = thy_ctxt
   1.201        (* add registrations *)
   1.202 -      |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss
   1.203 +(*      |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *)
   1.204 +      |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss
   1.205        (* add witnesses of Assumed elements (only those generate proof obligations) *)
   1.206 -      |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss)
   1.207 +      |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
   1.208        (* add equations *)
   1.209        |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
   1.210            (map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
   1.211 @@ -2084,6 +2083,23 @@
   1.212            (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
   1.213              | ((_, Derived _), _) => NONE) all_elemss);
   1.214  
   1.215 +    fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
   1.216 +        let
   1.217 +          val ctxt = mk_ctxt thy_ctxt;
   1.218 +          val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
   1.219 +              (Symtab.empty, Symtab.empty) prems eqns atts
   1.220 +              exp (attrib thy_ctxt) facts;
   1.221 +        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
   1.222 +      | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
   1.223 +
   1.224 +    fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
   1.225 +      let
   1.226 +        val (prfx_atts, _, _) = case get_reg thy_ctxt imp id
   1.227 +         of SOME x => x
   1.228 +          | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
   1.229 +              ^ " while activating facts.");
   1.230 +      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end;
   1.231 +
   1.232      val thy_ctxt'' = thy_ctxt'
   1.233        (* add witnesses of Derived elements *)
   1.234        |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
   1.235 @@ -2092,7 +2108,7 @@
   1.236  
   1.237      (* Accumulate equations *)
   1.238      val all_eqns =
   1.239 -      fold_map (join_eqns (get_reg thy_ctxt'' imp) (fst o fst) ctxt) all_elemss Termtab.empty
   1.240 +      fold_map (join_eqns (get_reg thy_ctxt'' imp) fst ctxt) all_propss Termtab.empty
   1.241        |> fst
   1.242        |> map (apsnd (map snd o Termtab.dest))
   1.243        |> (fn xs => fold Idtab.update xs Idtab.empty)
   1.244 @@ -2108,7 +2124,7 @@
   1.245               [([Element.conclude_witness thm], [])])] #> snd)
   1.246             (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms)
   1.247      (* add facts *)
   1.248 -    |> fold (activate_elems prems all_eqns exp) new_elemss
   1.249 +    |> fold (activate_elems all_eqns) new_elemss
   1.250    end;
   1.251  
   1.252  fun global_activate_facts_elemss x = gen_activate_facts_elemss