src/Pure/Isar/locale.ML
changeset 28739 bbb5f83ce602
parent 28734 19277c7a160c
child 28792 1d80cee865de
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Nov 13 14:19:09 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 13 14:19:10 2008 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4    val add_declaration: string -> declaration -> Proof.context -> Proof.context
     1.5  
     1.6    (* Interpretation *)
     1.7 -  val get_interpret_morph: theory -> string -> string ->
     1.8 +  val get_interpret_morph: theory -> string -> bool * string -> string ->
     1.9      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    1.10      string -> term list -> Morphism.morphism
    1.11    val interpretation_i: (Proof.context -> Proof.context) ->
    1.12 @@ -137,6 +137,37 @@
    1.13  fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
    1.14  
    1.15  
    1.16 +(* auxiliary: noting with structured name bindings *)
    1.17 +
    1.18 +fun global_note_prefix kind ((bnd, atts), facts_atts_s) thy =
    1.19 +  (*FIXME belongs to theory_target.ML*)
    1.20 +  let
    1.21 +    val prfx = Name.prefix_of bnd;
    1.22 +    val name = Name.name_of bnd;
    1.23 +  in
    1.24 +    thy
    1.25 +    |> Sign.qualified_names
    1.26 +    |> fold (fn (prfx_seg, sticky) =>
    1.27 +        (if sticky then Sign.sticky_prefix else Sign.add_path) prfx_seg) prfx
    1.28 +    |> yield_singleton (PureThy.note_thmss kind) ((Name.binding name, atts), facts_atts_s)
    1.29 +    ||> Sign.restore_naming thy
    1.30 +  end;
    1.31 +
    1.32 +fun local_note_prefix kind ((bnd, atts), facts_atts_s) ctxt =
    1.33 +  (*FIXME belongs to theory_target.ML ?*)
    1.34 +  let
    1.35 +    val prfx = Name.prefix_of bnd;
    1.36 +    val name = Name.name_of bnd;
    1.37 +  in
    1.38 +    ctxt
    1.39 +    |> ProofContext.qualified_names
    1.40 +    |> fold (fn (prfx_seg, sticky) =>
    1.41 +        (if sticky then ProofContext.sticky_prefix else ProofContext.add_path) prfx_seg) prfx
    1.42 +    |> yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding name, atts), facts_atts_s)
    1.43 +    ||> ProofContext.restore_naming ctxt
    1.44 +  end;
    1.45 +
    1.46 +
    1.47  (** locale elements and expressions **)
    1.48  
    1.49  datatype ctxt = datatype Element.ctxt;
    1.50 @@ -549,8 +580,8 @@
    1.51      val prt_thm = prt_term o prop_of;
    1.52      fun prt_inst ts =
    1.53          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
    1.54 -    fun prt_prfx ((false, prfx), pprfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str pprfx]
    1.55 -      | prt_prfx ((true, prfx), pprfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str pprfx];
    1.56 +    fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx]
    1.57 +      | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx];
    1.58      fun prt_eqns [] = Pretty.str "no equations."
    1.59        | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
    1.60            Pretty.breaks (map prt_thm eqns));
    1.61 @@ -945,8 +976,7 @@
    1.62          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    1.63          val elem_morphism =
    1.64            Element.rename_morphism ren $>
    1.65 -          Morphism.name_morphism
    1.66 -            (Name.map_name (NameSpace.qualified (param_prefix params))) $>
    1.67 +          Morphism.name_morphism (Name.add_prefix false (param_prefix params)) $>
    1.68            Element.instT_morphism thy env;
    1.69          val elems' = map (Element.morph_ctxt elem_morphism) elems;
    1.70        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
    1.71 @@ -1005,7 +1035,7 @@
    1.72    | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
    1.73        let
    1.74          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.75 -        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
    1.76 +        val (res, ctxt') = ctxt |> fold_map (local_note_prefix kind) facts';
    1.77        in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
    1.78  
    1.79  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
    1.80 @@ -1586,37 +1616,6 @@
    1.81  
    1.82  (** store results **)
    1.83  
    1.84 -(* naming of interpreted theorems *)
    1.85 -
    1.86 -fun global_note_prefix kind ((bnd, atts), facts_atts_s) thy =
    1.87 -  (*FIXME belongs to theory_target.ML*)
    1.88 -  let
    1.89 -    val prfx = Name.prefix_of bnd;
    1.90 -    val name = Name.name_of bnd;
    1.91 -  in
    1.92 -    thy
    1.93 -    |> Sign.qualified_names
    1.94 -    |> fold (fn (prfx_seg, fully_qualified) =>
    1.95 -        (if fully_qualified then Sign.sticky_prefix else Sign.add_path) prfx_seg) prfx
    1.96 -    |> yield_singleton (PureThy.note_thmss kind) ((Name.binding name, atts), facts_atts_s)
    1.97 -    ||> Sign.restore_naming thy
    1.98 -  end;
    1.99 -
   1.100 -fun local_note_prefix kind ((bnd, atts), facts_atts_s) ctxt =
   1.101 -  (*FIXME belongs to theory_target.ML ?*)
   1.102 -  let
   1.103 -    val prfx = Name.prefix_of bnd;
   1.104 -    val name = Name.name_of bnd;
   1.105 -  in
   1.106 -    ctxt
   1.107 -    |> ProofContext.qualified_names
   1.108 -    |> fold (fn (prfx_seg, fully_qualified) =>
   1.109 -        (if fully_qualified then ProofContext.sticky_prefix else ProofContext.add_path) prfx_seg) prfx
   1.110 -    |> yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding name, atts), facts_atts_s)
   1.111 -    ||> ProofContext.restore_naming ctxt
   1.112 -  end;
   1.113 -
   1.114 -
   1.115  (* join equations of an id with already accumulated ones *)
   1.116  
   1.117  fun join_eqns get_reg id eqns =
   1.118 @@ -1656,9 +1655,16 @@
   1.119    in ((tinst, inst), wits, eqns) end;
   1.120  
   1.121  
   1.122 -(* compute morphism and apply to args *)
   1.123 -
   1.124 -fun inst_morph thy prfx param_prfx insts prems eqns export =
   1.125 +(* compute and apply morphism *)
   1.126 +
   1.127 +fun add_prefixes loc (sticky, interp_prfx) param_prfx bnd =
   1.128 +  bnd
   1.129 +  |> (if sticky andalso Name.name_of bnd <> "" andalso param_prfx <> ""
   1.130 +        then Name.add_prefix false param_prfx else I)
   1.131 +  |> Name.add_prefix sticky interp_prfx
   1.132 +  |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
   1.133 +
   1.134 +fun inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns export =
   1.135    let
   1.136      (* standardise export morphism *)
   1.137      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
   1.138 @@ -1668,46 +1674,29 @@
   1.139      val export' =
   1.140        Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   1.141    in
   1.142 -    Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
   1.143 +    Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx) $>
   1.144        Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   1.145        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   1.146        Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
   1.147        export'
   1.148    end;
   1.149  
   1.150 -fun morph_ctxt' phi = Element.map_ctxt
   1.151 -  {name = I,
   1.152 -   var = Morphism.var phi,
   1.153 -   typ = Morphism.typ phi,
   1.154 -   term = Morphism.term phi,
   1.155 -   fact = Morphism.fact phi,
   1.156 -   attrib = Args.morph_values phi};
   1.157 -
   1.158 -fun add_prefixes loc (fully_qualified, interp_prfx) pprfx bnd =
   1.159 -  bnd
   1.160 -  |> (if fully_qualified andalso Name.name_of bnd <> "" andalso pprfx <> ""
   1.161 -        then Name.add_prefix false pprfx else I)
   1.162 -  |> Name.add_prefix fully_qualified interp_prfx
   1.163 -  |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
   1.164 -
   1.165 -fun interpret_args thy loc (fully_qualified, interp_prfx) pprfx inst attrib args =
   1.166 -  args
   1.167 -  |> Element.facts_map (morph_ctxt' inst)
   1.168 -       (*FIXME: morph_ctxt' suppresses application of name morphism.*)
   1.169 -  |> Attrib.map_facts attrib
   1.170 -  |> (map o apfst o apfst) (add_prefixes loc (fully_qualified, interp_prfx) pprfx);
   1.171 +fun activate_note thy loc (sticky, interp_prfx) param_prfx attrib insts prems eqns exp =
   1.172 +  (Element.facts_map o Element.morph_ctxt)
   1.173 +      (inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns exp)
   1.174 +  #> Attrib.map_facts attrib (*o Args.morph_values (Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx))*);
   1.175  
   1.176  
   1.177  (* public interface to interpretation morphism *)
   1.178  
   1.179 -fun get_interpret_morph thy prfx param_prfx (exp, imp) target ext_ts =
   1.180 +fun get_interpret_morph thy loc (sticky, interp_prfx) param_prfx (exp, imp) target ext_ts =
   1.181    let
   1.182      val parms = the_locale thy target |> #params |> map fst;
   1.183      val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.184        (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
   1.185      val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   1.186    in
   1.187 -    inst_morph thy prfx param_prfx insts prems eqns exp
   1.188 +    inst_morph thy loc (sticky, interp_prfx) param_prfx insts prems eqns exp
   1.189    end;
   1.190  
   1.191  (* store instantiations of args for all registered interpretations
   1.192 @@ -1722,13 +1711,12 @@
   1.193      val regs = get_global_registrations thy target;
   1.194      (* add args to thy for all registrations *)
   1.195  
   1.196 -    fun activate (ext_ts, (((fully_qualified, interp_prfx), pprfx), (exp, imp), _, _)) thy =
   1.197 +    fun activate (ext_ts, (((sticky, interp_prfx), param_prfx), (exp, imp), _, _)) thy =
   1.198        let
   1.199          val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   1.200 -        val attrib = Attrib.attribute_i thy;
   1.201          val args' = args
   1.202 -          |> interpret_args thy target (fully_qualified, interp_prfx) pprfx
   1.203 -               (inst_morph thy interp_prfx pprfx insts prems eqns exp) attrib;
   1.204 +          |> activate_note thy target (sticky, interp_prfx) param_prfx
   1.205 +               (Attrib.attribute_i thy) insts prems eqns exp;
   1.206        in
   1.207          thy
   1.208          |> fold (snd oo global_note_prefix kind) args'
   1.209 @@ -2102,7 +2090,7 @@
   1.210  
   1.211  (* activate instantiated facts in theory or context *)
   1.212  
   1.213 -fun gen_activate_facts_elemss mk_ctxt note note_interp attrib put_reg add_wit add_eqn
   1.214 +fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
   1.215          prfx all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
   1.216    let
   1.217      val ctxt = mk_ctxt thy_ctxt;
   1.218 @@ -2139,50 +2127,46 @@
   1.219           (map_filter (fn ((_, Assumed _), _) => NONE
   1.220              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
   1.221  
   1.222 -    fun activate_elem loc (fully_qualified, interp_prfx) pprfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
   1.223 +    fun activate_elem loc (sticky, interp_prfx) param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
   1.224          let
   1.225            val ctxt = mk_ctxt thy_ctxt;
   1.226            val thy = ProofContext.theory_of ctxt;
   1.227            val facts' = facts
   1.228 -            |> interpret_args (ProofContext.theory_of ctxt) loc
   1.229 -                 (fully_qualified, interp_prfx) pprfx
   1.230 -                   (inst_morph thy interp_prfx pprfx insts prems eqns exp) (attrib thy_ctxt);
   1.231 +            |> activate_note thy loc (sticky, interp_prfx) param_prfx
   1.232 +                 (attrib thy_ctxt) insts prems eqns exp;
   1.233          in 
   1.234            thy_ctxt
   1.235 -          |> fold (snd oo note_interp kind) facts'
   1.236 +          |> fold (snd oo note kind) facts'
   1.237          end
   1.238        | activate_elem _ _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
   1.239  
   1.240 -    fun activate_elems ((((loc, ext_ts), _), _), ps) thy_ctxt =
   1.241 +    fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
   1.242        let
   1.243          val ctxt = mk_ctxt thy_ctxt;
   1.244          val thy = ProofContext.theory_of ctxt;
   1.245          val {params, elems, ...} = the_locale thy loc;
   1.246          val parms = map fst params;
   1.247 -        val pprfx = param_prefix ps;
   1.248 +        val param_prfx = param_prefix ps;
   1.249          val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.250            (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
   1.251          val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
   1.252        in
   1.253          thy_ctxt
   1.254 -        |> fold (activate_elem loc prfx pprfx insts prems eqns exp o fst) elems
   1.255 +        |> fold (activate_elem loc prfx param_prfx insts prems eqns exp o fst) elems
   1.256        end;
   1.257  
   1.258    in
   1.259      thy_ctxt''
   1.260      (* add equations as lemmas to context *)
   1.261 -    |> fold (fn (attns, thms) =>
   1.262 -         fold (fn (attn, thm) => note "lemma"
   1.263 -           [(apsnd (map (attrib thy_ctxt'')) attn,
   1.264 -             [([Element.conclude_witness thm], [])])] #> snd)
   1.265 -           (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms)
   1.266 +    |> (fold2 o fold2) (fn attn => fn thm => snd o note Thm.lemmaK
   1.267 +         ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
   1.268 +            (unflat eq_thms eq_attns) eq_thms
   1.269      (* add interpreted facts *)
   1.270 -    |> fold activate_elems (new_elemss ~~ new_pss)
   1.271 +    |> fold2 activate_elems new_elemss new_pss
   1.272    end;
   1.273  
   1.274  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   1.275    ProofContext.init
   1.276 -  PureThy.note_thmss
   1.277    global_note_prefix
   1.278    Attrib.attribute_i
   1.279    put_global_registration
   1.280 @@ -2192,7 +2176,6 @@
   1.281  
   1.282  fun local_activate_facts_elemss x = gen_activate_facts_elemss
   1.283    I
   1.284 -  ProofContext.note_thmss_i
   1.285    local_note_prefix
   1.286    (Attrib.attribute_i o ProofContext.theory_of)
   1.287    put_local_registration
   1.288 @@ -2373,7 +2356,8 @@
   1.289            the target, unless already present
   1.290          - add facts of induced registrations to theory **)
   1.291  
   1.292 -    fun activate thmss thy = let
   1.293 +    fun activate thmss thy =
   1.294 +      let
   1.295          val satisfy = Element.satisfy_thm (flat thmss);
   1.296          val ids_elemss_thmss = ids_elemss ~~ thmss;
   1.297          val regs = get_global_registrations thy target;
   1.298 @@ -2383,11 +2367,10 @@
   1.299                  |> fold (add_witness_in_locale target id) thms
   1.300            | activate_id _ thy = thy;
   1.301  
   1.302 -        fun activate_reg (ext_ts, (((fully_qualified, interp_prfx), pprfx), (exp, imp), _, _)) thy =
   1.303 +        fun activate_reg (ext_ts, (((sticky, interp_prfx), param_prfx), (exp, imp), _, _)) thy =
   1.304            let
   1.305              val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
   1.306 -            fun inst_parms ps = map
   1.307 -                  (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts)) ps;
   1.308 +            val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
   1.309              val disch = Element.satisfy_thm wits;
   1.310              val new_elemss = filter (fn (((name, ps), _), _) =>
   1.311                  not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
   1.312 @@ -2398,7 +2381,7 @@
   1.313                  if test_global_registration thy (name, ps')
   1.314                  then thy
   1.315                  else thy
   1.316 -                  |> put_global_registration (name, ps') ((fully_qualified, interp_prfx), param_prefix ps) (exp, imp)
   1.317 +                  |> put_global_registration (name, ps') ((sticky, interp_prfx), param_prefix ps) (exp, imp)
   1.318                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.319                       (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
   1.320                end;
   1.321 @@ -2410,40 +2393,24 @@
   1.322                  if test_global_registration thy (name, ps')
   1.323                  then thy
   1.324                  else thy
   1.325 -                  |> put_global_registration (name, ps') ((fully_qualified, interp_prfx), param_prefix ps) (exp, imp)
   1.326 +                  |> put_global_registration (name, ps') ((sticky, interp_prfx), param_prefix ps) (exp, imp)
   1.327                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.328                         (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
   1.329                         (Element.inst_term insts t,
   1.330                          disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
   1.331                end;
   1.332  
   1.333 -            fun apply_prefix loc bnd =
   1.334 -              let
   1.335 -                val param_prfx_name = Name.name_of bnd;
   1.336 -                val (param_prfx, name) = case NameSpace.explode param_prfx_name
   1.337 -                 of [] => ([], "")
   1.338 -                  | [name] => ([], name) (*heuristic for locales with no parameter*)
   1.339 -                  | prfx :: name_segs => (if fully_qualified then [(prfx, false)] else [],
   1.340 -                       NameSpace.implode name_segs);
   1.341 -              in
   1.342 -                Name.binding name
   1.343 -                |> fold (uncurry Name.add_prefix o swap) param_prfx
   1.344 -                |> Name.add_prefix fully_qualified interp_prfx
   1.345 -                |> Name.add_prefix false (NameSpace.base loc ^ "_locale")
   1.346 -              end;
   1.347 -
   1.348              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
   1.349                  let
   1.350                    val att_morphism =
   1.351 -                    Morphism.name_morphism (Name.qualified interp_prfx) $>
   1.352 -                      (* FIXME? treatment of parameter prefix *)
   1.353 +                    Morphism.name_morphism (add_prefixes loc (sticky, interp_prfx) param_prfx) $>
   1.354                      Morphism.thm_morphism satisfy $>
   1.355                      Element.inst_morphism thy insts $>
   1.356                      Morphism.thm_morphism disch;
   1.357                    val facts' = facts
   1.358                      |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
   1.359                      |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
   1.360 -                    |> (map o apfst o apfst) (apply_prefix loc);
   1.361 +                    |> (map o apfst o apfst) (add_prefixes loc (sticky, interp_prfx) param_prfx);
   1.362                  in
   1.363                    thy
   1.364                    |> fold (snd oo global_note_prefix kind) facts'