using explicit interpretaton prefix in Name.binding (still on the surface)
authorhaftmann
Mon Nov 10 08:18:58 2008 +0100 (2008-11-10)
changeset 2872647ff45771f2c
parent 28725 4a71cc58b203
child 28727 185110a4b97a
using explicit interpretaton prefix in Name.binding (still on the surface)
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Nov 10 08:18:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Nov 10 08:18:58 2008 +0100
     1.3 @@ -1590,25 +1590,53 @@
     1.4  
     1.5  (* naming of interpreted theorems *)
     1.6  
     1.7 +fun global_note_prefix kind ((bnd, atts), facts_atts_s) thy =
     1.8 +  let
     1.9 +    val prfx = Name.prefix_of bnd;
    1.10 +    val name = Name.name_of bnd;
    1.11 +  in
    1.12 +    thy
    1.13 +    |> Sign.qualified_names
    1.14 +    |> fold (fn (prfx_seg, fully_qualified) =>
    1.15 +        (if fully_qualified then Sign.sticky_prefix else Sign.add_path) prfx_seg) prfx
    1.16 +    |> yield_singleton (PureThy.note_thmss kind) ((Name.binding name, atts), facts_atts_s)
    1.17 +    ||> Sign.restore_naming thy
    1.18 +  end;
    1.19 +
    1.20 +fun local_note_prefix kind ((bnd, atts), facts_atts_s) ctxt =
    1.21 +  let
    1.22 +    val prfx = Name.prefix_of bnd;
    1.23 +    val name = Name.name_of bnd;
    1.24 +  in
    1.25 +    ctxt
    1.26 +    |> ProofContext.qualified_names
    1.27 +    |> fold (fn (prfx_seg, fully_qualified) =>
    1.28 +        (if fully_qualified then ProofContext.sticky_prefix else ProofContext.add_path) prfx_seg) prfx
    1.29 +    |> yield_singleton (ProofContext.note_thmss_i kind) ((Name.binding name, atts), facts_atts_s)
    1.30 +    ||> ProofContext.restore_naming ctxt
    1.31 +  end;
    1.32 +
    1.33  fun add_param_prefixss s = (map o apfst o apfst) (Name.qualified s);
    1.34 -fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
    1.35 -  (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
    1.36 -
    1.37 -fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
    1.38 -  thy
    1.39 -  |> Sign.qualified_names
    1.40 -  |> Sign.add_path (NameSpace.base loc ^ "_locale")
    1.41 -  |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    1.42 -  |> PureThy.note_thmss kind (if fully_qualified then args else drop_param_prefixss args)
    1.43 -  ||> Sign.restore_naming thy;
    1.44 -
    1.45 -fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    1.46 -  ctxt
    1.47 -  |> ProofContext.qualified_names
    1.48 -  |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
    1.49 -  |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
    1.50 -  |> ProofContext.note_thmss_i kind (if fully_qualified then args else drop_param_prefixss args)
    1.51 -  ||> ProofContext.restore_naming ctxt;
    1.52 +
    1.53 +fun apply_prefix loc (fully_qualified, interp_prfx) ((bnd, atts), facts_atts_s) =
    1.54 +  let
    1.55 +    val param_prfx_name = Name.name_of bnd;
    1.56 +    val (param_prfx, name) = case NameSpace.explode param_prfx_name
    1.57 +     of [] => ([], "")
    1.58 +      | [name] => ([], name) (*heuristic for locales with no parameter*)
    1.59 +      | prfx :: name_segs => (if fully_qualified then [(prfx, false)] else [],
    1.60 +           NameSpace.implode name_segs);
    1.61 +    val bnd' = Name.binding name
    1.62 +      |> fold (uncurry Name.add_prefix o swap) param_prfx
    1.63 +      |> Name.add_prefix fully_qualified interp_prfx
    1.64 +      |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
    1.65 +  in ((bnd', atts), facts_atts_s) end;
    1.66 +
    1.67 +fun global_note_prefix' kind loc (fully_qualified, interp_prfx) =
    1.68 +  fold_map (global_note_prefix kind o apply_prefix loc (fully_qualified, interp_prfx));
    1.69 +
    1.70 +fun local_note_prefix' kind loc (fully_qualified, interp_prfx) =
    1.71 +  fold_map (local_note_prefix kind o apply_prefix loc (fully_qualified, interp_prfx));
    1.72  
    1.73  
    1.74  (* join equations of an id with already accumulated ones *)
    1.75 @@ -1712,7 +1740,7 @@
    1.76          val args' = args
    1.77            |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns exp) attrib
    1.78            |> add_param_prefixss pprfx;
    1.79 -      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
    1.80 +      in global_note_prefix' kind target (fully_qualified, prfx) args' thy |> snd end;
    1.81    in fold activate regs thy end;
    1.82  
    1.83  
    1.84 @@ -2158,7 +2186,7 @@
    1.85  fun global_activate_facts_elemss x = gen_activate_facts_elemss
    1.86        ProofContext.init
    1.87        PureThy.note_thmss
    1.88 -      global_note_prefix_i
    1.89 +      global_note_prefix'
    1.90        Attrib.attribute_i
    1.91        put_global_registration
    1.92        add_global_witness
    1.93 @@ -2168,7 +2196,7 @@
    1.94  fun local_activate_facts_elemss x = gen_activate_facts_elemss
    1.95        I
    1.96        ProofContext.note_thmss_i
    1.97 -      local_note_prefix_i
    1.98 +      local_note_prefix'
    1.99        (Attrib.attribute_i o ProofContext.theory_of)
   1.100        put_local_registration
   1.101        add_local_witness
   1.102 @@ -2405,7 +2433,7 @@
   1.103                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   1.104                  in
   1.105                    thy
   1.106 -                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
   1.107 +                  |> global_note_prefix' kind loc (fully_qualified, prfx) facts'
   1.108                    |> snd
   1.109                  end
   1.110                | activate_elem _ _ thy = thy;