restruced naming code in anticipation of introduction of name morphisms
authorhaftmann
Mon Nov 10 19:42:22 2008 +0100 (2008-11-10)
changeset 2873419277c7a160c
parent 28733 18ffcbf1b3ae
child 28735 bed31381e6b6
restruced naming code in anticipation of introduction of name morphisms
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Nov 10 19:42:21 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Nov 10 19:42:22 2008 +0100
     1.3 @@ -650,10 +650,7 @@
     1.4  fun params_of' elemss =
     1.5    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
     1.6  
     1.7 -
     1.8  fun param_prefix params = space_implode "_" params;
     1.9 -fun params_qualified params name =
    1.10 -  NameSpace.qualified (param_prefix params) name;
    1.11  
    1.12  
    1.13  (* CB: param_types has the following type:
    1.14 @@ -948,7 +945,8 @@
    1.15          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    1.16          val elem_morphism =
    1.17            Element.rename_morphism ren $>
    1.18 -          Morphism.name_morphism (Name.map_name (params_qualified params)) $>
    1.19 +          Morphism.name_morphism
    1.20 +            (Name.map_name (NameSpace.qualified (param_prefix params))) $>
    1.21            Element.instT_morphism thy env;
    1.22          val elems' = map (Element.morph_ctxt elem_morphism) elems;
    1.23        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
    1.24 @@ -1591,6 +1589,7 @@
    1.25  (* naming of interpreted theorems *)
    1.26  
    1.27  fun global_note_prefix kind ((bnd, atts), facts_atts_s) thy =
    1.28 +  (*FIXME belongs to theory_target.ML*)
    1.29    let
    1.30      val prfx = Name.prefix_of bnd;
    1.31      val name = Name.name_of bnd;
    1.32 @@ -1604,6 +1603,7 @@
    1.33    end;
    1.34  
    1.35  fun local_note_prefix kind ((bnd, atts), facts_atts_s) ctxt =
    1.36 +  (*FIXME belongs to theory_target.ML ?*)
    1.37    let
    1.38      val prfx = Name.prefix_of bnd;
    1.39      val name = Name.name_of bnd;
    1.40 @@ -1616,28 +1616,6 @@
    1.41      ||> ProofContext.restore_naming ctxt
    1.42    end;
    1.43  
    1.44 -fun add_param_prefixss s = (map o apfst o apfst) (Name.qualified s);
    1.45 -
    1.46 -fun apply_prefix loc (fully_qualified, interp_prfx) ((bnd, atts), facts_atts_s) =
    1.47 -  let
    1.48 -    val param_prfx_name = Name.name_of bnd;
    1.49 -    val (param_prfx, name) = case NameSpace.explode param_prfx_name
    1.50 -     of [] => ([], "")
    1.51 -      | [name] => ([], name) (*heuristic for locales with no parameter*)
    1.52 -      | prfx :: name_segs => (if fully_qualified then [(prfx, false)] else [],
    1.53 -           NameSpace.implode name_segs);
    1.54 -    val bnd' = Name.binding name
    1.55 -      |> fold (uncurry Name.add_prefix o swap) param_prfx
    1.56 -      |> Name.add_prefix fully_qualified interp_prfx
    1.57 -      |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
    1.58 -  in ((bnd', atts), facts_atts_s) end;
    1.59 -
    1.60 -fun global_note_prefix' kind loc (fully_qualified, interp_prfx) =
    1.61 -  fold_map (global_note_prefix kind o apply_prefix loc (fully_qualified, interp_prfx));
    1.62 -
    1.63 -fun local_note_prefix' kind loc (fully_qualified, interp_prfx) =
    1.64 -  fold_map (local_note_prefix kind o apply_prefix loc (fully_qualified, interp_prfx));
    1.65 -
    1.66  
    1.67  (* join equations of an id with already accumulated ones *)
    1.68  
    1.69 @@ -1705,9 +1683,20 @@
    1.70     fact = Morphism.fact phi,
    1.71     attrib = Args.morph_values phi};
    1.72  
    1.73 -fun interpret_args thy inst attrib args =
    1.74 -  args |> Element.facts_map (morph_ctxt' inst) |> Attrib.map_facts attrib;
    1.75 -    (* morph_ctxt' suppresses application of name morphism.  FIXME *)
    1.76 +fun add_prefixes loc (fully_qualified, interp_prfx) pprfx bnd =
    1.77 +  bnd
    1.78 +  |> (if fully_qualified andalso Name.name_of bnd <> "" andalso pprfx <> ""
    1.79 +        then Name.add_prefix false pprfx else I)
    1.80 +  |> Name.add_prefix fully_qualified interp_prfx
    1.81 +  |> Name.add_prefix false (NameSpace.base loc ^ "_locale");
    1.82 +
    1.83 +fun interpret_args thy loc (fully_qualified, interp_prfx) pprfx inst attrib args =
    1.84 +  args
    1.85 +  |> Element.facts_map (morph_ctxt' inst)
    1.86 +       (*FIXME: morph_ctxt' suppresses application of name morphism.*)
    1.87 +  |> Attrib.map_facts attrib
    1.88 +  |> (map o apfst o apfst) (add_prefixes loc (fully_qualified, interp_prfx) pprfx);
    1.89 +
    1.90  
    1.91  (* public interface to interpretation morphism *)
    1.92  
    1.93 @@ -1733,14 +1722,17 @@
    1.94      val regs = get_global_registrations thy target;
    1.95      (* add args to thy for all registrations *)
    1.96  
    1.97 -    fun activate (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy =
    1.98 +    fun activate (ext_ts, (((fully_qualified, interp_prfx), pprfx), (exp, imp), _, _)) thy =
    1.99        let
   1.100          val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   1.101          val attrib = Attrib.attribute_i thy;
   1.102          val args' = args
   1.103 -          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns exp) attrib
   1.104 -          |> add_param_prefixss pprfx;
   1.105 -      in global_note_prefix' kind target (fully_qualified, prfx) args' thy |> snd end;
   1.106 +          |> interpret_args thy target (fully_qualified, interp_prfx) pprfx
   1.107 +               (inst_morph thy interp_prfx pprfx insts prems eqns exp) attrib;
   1.108 +      in
   1.109 +        thy
   1.110 +        |> fold (snd oo global_note_prefix kind) args'
   1.111 +      end;
   1.112    in fold activate regs thy end;
   1.113  
   1.114  
   1.115 @@ -2147,14 +2139,19 @@
   1.116           (map_filter (fn ((_, Assumed _), _) => NONE
   1.117              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
   1.118  
   1.119 -    fun activate_elem inst loc prfx pprfx (Notes (kind, facts)) thy_ctxt =
   1.120 +    fun activate_elem loc (fully_qualified, interp_prfx) pprfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
   1.121          let
   1.122            val ctxt = mk_ctxt thy_ctxt;
   1.123 -          val facts' = facts |>
   1.124 -              interpret_args (ProofContext.theory_of ctxt) inst (attrib thy_ctxt) |>
   1.125 -              add_param_prefixss pprfx;
   1.126 -        in snd (note_interp kind loc prfx facts' thy_ctxt) end
   1.127 -      | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
   1.128 +          val thy = ProofContext.theory_of ctxt;
   1.129 +          val facts' = facts
   1.130 +            |> interpret_args (ProofContext.theory_of ctxt) loc
   1.131 +                 (fully_qualified, interp_prfx) pprfx
   1.132 +                   (inst_morph thy interp_prfx pprfx insts prems eqns exp) (attrib thy_ctxt);
   1.133 +        in 
   1.134 +          thy_ctxt
   1.135 +          |> fold (snd oo note_interp kind) facts'
   1.136 +        end
   1.137 +      | activate_elem _ _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
   1.138  
   1.139      fun activate_elems ((((loc, ext_ts), _), _), ps) thy_ctxt =
   1.140        let
   1.141 @@ -2166,9 +2163,9 @@
   1.142          val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.143            (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
   1.144          val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
   1.145 -        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns exp;
   1.146        in
   1.147 -        fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt
   1.148 +        thy_ctxt
   1.149 +        |> fold (activate_elem loc prfx pprfx insts prems eqns exp o fst) elems
   1.150        end;
   1.151  
   1.152    in
   1.153 @@ -2184,24 +2181,24 @@
   1.154    end;
   1.155  
   1.156  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   1.157 -      ProofContext.init
   1.158 -      PureThy.note_thmss
   1.159 -      global_note_prefix'
   1.160 -      Attrib.attribute_i
   1.161 -      put_global_registration
   1.162 -      add_global_witness
   1.163 -      add_global_equation
   1.164 -      x;
   1.165 +  ProofContext.init
   1.166 +  PureThy.note_thmss
   1.167 +  global_note_prefix
   1.168 +  Attrib.attribute_i
   1.169 +  put_global_registration
   1.170 +  add_global_witness
   1.171 +  add_global_equation
   1.172 +  x;
   1.173  
   1.174  fun local_activate_facts_elemss x = gen_activate_facts_elemss
   1.175 -      I
   1.176 -      ProofContext.note_thmss_i
   1.177 -      local_note_prefix'
   1.178 -      (Attrib.attribute_i o ProofContext.theory_of)
   1.179 -      put_local_registration
   1.180 -      add_local_witness
   1.181 -      add_local_equation
   1.182 -      x;
   1.183 +  I
   1.184 +  ProofContext.note_thmss_i
   1.185 +  local_note_prefix
   1.186 +  (Attrib.attribute_i o ProofContext.theory_of)
   1.187 +  put_local_registration
   1.188 +  add_local_witness
   1.189 +  add_local_equation
   1.190 +  x;
   1.191  
   1.192  fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
   1.193    let
   1.194 @@ -2386,7 +2383,7 @@
   1.195                  |> fold (add_witness_in_locale target id) thms
   1.196            | activate_id _ thy = thy;
   1.197  
   1.198 -        fun activate_reg (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy =
   1.199 +        fun activate_reg (ext_ts, (((fully_qualified, interp_prfx), pprfx), (exp, imp), _, _)) thy =
   1.200            let
   1.201              val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
   1.202              fun inst_parms ps = map
   1.203 @@ -2401,7 +2398,7 @@
   1.204                  if test_global_registration thy (name, ps')
   1.205                  then thy
   1.206                  else thy
   1.207 -                  |> put_global_registration (name, ps') ((fully_qualified, prfx), param_prefix ps) (exp, imp)
   1.208 +                  |> put_global_registration (name, ps') ((fully_qualified, interp_prfx), param_prefix ps) (exp, imp)
   1.209                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.210                       (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
   1.211                end;
   1.212 @@ -2413,28 +2410,43 @@
   1.213                  if test_global_registration thy (name, ps')
   1.214                  then thy
   1.215                  else thy
   1.216 -                  |> put_global_registration (name, ps') ((fully_qualified, prfx), param_prefix ps) (exp, imp)
   1.217 +                  |> put_global_registration (name, ps') ((fully_qualified, interp_prfx), param_prefix ps) (exp, imp)
   1.218                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.219                         (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
   1.220                         (Element.inst_term insts t,
   1.221                          disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
   1.222                end;
   1.223  
   1.224 +            fun apply_prefix loc bnd =
   1.225 +              let
   1.226 +                val param_prfx_name = Name.name_of bnd;
   1.227 +                val (param_prfx, name) = case NameSpace.explode param_prfx_name
   1.228 +                 of [] => ([], "")
   1.229 +                  | [name] => ([], name) (*heuristic for locales with no parameter*)
   1.230 +                  | prfx :: name_segs => (if fully_qualified then [(prfx, false)] else [],
   1.231 +                       NameSpace.implode name_segs);
   1.232 +              in
   1.233 +                Name.binding name
   1.234 +                |> fold (uncurry Name.add_prefix o swap) param_prfx
   1.235 +                |> Name.add_prefix fully_qualified interp_prfx
   1.236 +                |> Name.add_prefix false (NameSpace.base loc ^ "_locale")
   1.237 +              end;
   1.238 +
   1.239              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
   1.240                  let
   1.241                    val att_morphism =
   1.242 -                    Morphism.name_morphism (Name.qualified prfx) $>
   1.243 -(* FIXME? treatment of parameter prefix *)
   1.244 +                    Morphism.name_morphism (Name.qualified interp_prfx) $>
   1.245 +                      (* FIXME? treatment of parameter prefix *)
   1.246                      Morphism.thm_morphism satisfy $>
   1.247                      Element.inst_morphism thy insts $>
   1.248                      Morphism.thm_morphism disch;
   1.249                    val facts' = facts
   1.250                      |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
   1.251 -                    |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   1.252 +                    |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
   1.253 +                    |> (map o apfst o apfst) (apply_prefix loc);
   1.254                  in
   1.255                    thy
   1.256 -                  |> global_note_prefix' kind loc (fully_qualified, prfx) facts'
   1.257 -                  |> snd
   1.258 +                  |> fold (snd oo global_note_prefix kind) facts'
   1.259                  end
   1.260                | activate_elem _ _ thy = thy;
   1.261