src/Pure/Isar/locale.ML
changeset 28083 103d9282a946
parent 28053 a2106c0d8c45
child 28084 a05ca48ef263
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -55,16 +55,16 @@
     1.4    val parameters_of_expr: theory -> expr ->
     1.5      ((string * typ) * mixfix) list
     1.6    val local_asms_of: theory -> string ->
     1.7 -    ((string * Attrib.src list) * term list) list
     1.8 +    ((Name.binding * Attrib.src list) * term list) list
     1.9    val global_asms_of: theory -> string ->
    1.10 -    ((string * Attrib.src list) * term list) list
    1.11 +    ((Name.binding * Attrib.src list) * term list) list
    1.12  
    1.13    (* Theorems *)
    1.14    val intros: theory -> string -> thm list * thm list
    1.15    val dests: theory -> string -> thm list
    1.16    (* Not part of the official interface.  DO NOT USE *)
    1.17    val facts_of: theory -> string
    1.18 -    -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list list
    1.19 +    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
    1.20  
    1.21    (* Processing of locale statements *)
    1.22    val read_context_statement: xstring option -> Element.context element list ->
    1.23 @@ -96,7 +96,7 @@
    1.24  
    1.25    (* Storing results *)
    1.26    val add_thmss: string -> string ->
    1.27 -    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.28 +    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.29      Proof.context -> Proof.context
    1.30    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
    1.31    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
    1.32 @@ -104,21 +104,21 @@
    1.33  
    1.34    val interpretation_i: (Proof.context -> Proof.context) ->
    1.35      (bool * string) * Attrib.src list -> expr ->
    1.36 -    term option list * ((bstring * Attrib.src list) * term) list ->
    1.37 +    term option list * ((Name.binding * Attrib.src list) * term) list ->
    1.38      theory -> Proof.state
    1.39    val interpretation: (Proof.context -> Proof.context) ->
    1.40      (bool * string) * Attrib.src list -> expr ->
    1.41 -    string option list * ((bstring * Attrib.src list) * string) list ->
    1.42 +    string option list * ((Name.binding * Attrib.src list) * string) list ->
    1.43      theory -> Proof.state
    1.44    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    1.45      xstring * expr -> theory -> Proof.state
    1.46    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    1.47      (bool * string) * Attrib.src list -> expr ->
    1.48 -    term option list * ((bstring * Attrib.src list) * term) list ->
    1.49 +    term option list * ((Name.binding * Attrib.src list) * term) list ->
    1.50      bool -> Proof.state -> Proof.state
    1.51    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    1.52      (bool * string) * Attrib.src list -> expr ->
    1.53 -    string option list * ((bstring * Attrib.src list) * string) list ->
    1.54 +    string option list * ((Name.binding * Attrib.src list) * string) list ->
    1.55      bool -> Proof.state -> Proof.state
    1.56  end;
    1.57  
    1.58 @@ -756,7 +756,7 @@
    1.59              val ren = renaming xs parms';
    1.60              (* renaming may reduce number of parameters *)
    1.61              val new_parms = map (Element.rename ren) parms' |> distinct (op =);
    1.62 -            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
    1.63 +            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
    1.64              val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
    1.65                  handle Symtab.DUP x =>
    1.66                    err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
    1.67 @@ -789,7 +789,7 @@
    1.68  fun make_raw_params_elemss (params, tenv, syn) =
    1.69      [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
    1.70        Int [Fixes (map (fn p =>
    1.71 -        (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
    1.72 +        (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
    1.73  
    1.74  
    1.75  (* flatten_expr:
    1.76 @@ -929,7 +929,7 @@
    1.77          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    1.78          val elem_morphism =
    1.79            Element.rename_morphism ren $>
    1.80 -          Morphism.name_morphism (params_qualified params) $>
    1.81 +          Morphism.name_morphism (Name.map_name (params_qualified params)) $>
    1.82            Element.instT_morphism thy env;
    1.83          val elems' = map (Element.morph_ctxt elem_morphism) elems;
    1.84        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
    1.85 @@ -978,7 +978,7 @@
    1.86          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    1.87          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    1.88              let val ((c, _), t') = LocalDefs.cert_def ctxt t
    1.89 -            in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
    1.90 +            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
    1.91          val (_, ctxt') =
    1.92            ctxt |> fold (Variable.auto_fixes o #1) asms
    1.93            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
    1.94 @@ -989,7 +989,7 @@
    1.95        let
    1.96          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.97          val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
    1.98 -      in (if is_ext then res else [], (ctxt', mode)) end;
    1.99 +      in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
   1.100  
   1.101  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
   1.102    let
   1.103 @@ -1076,15 +1076,15 @@
   1.104  *)
   1.105  
   1.106  fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
   1.107 -        val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
   1.108 +        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
   1.109        in
   1.110          ((ids',
   1.111           merge_syntax ctxt ids'
   1.112 -           (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
   1.113 +           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
   1.114             handle Symtab.DUP x => err_in_locale ctxt
   1.115               ("Conflicting syntax for parameter: " ^ quote x)
   1.116               (map #1 ids')),
   1.117 -         [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
   1.118 +         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
   1.119        end
   1.120    | flatten _ ((ids, syn), Elem elem) =
   1.121        ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
   1.122 @@ -1104,7 +1104,7 @@
   1.123        let val (vars, _) = prep_vars fixes ctxt
   1.124        in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
   1.125    | declare_ext_elem prep_vars (Constrains csts) ctxt =
   1.126 -      let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
   1.127 +      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
   1.128        in ([], ctxt') end
   1.129    | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
   1.130    | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
   1.131 @@ -1227,8 +1227,9 @@
   1.132        end;
   1.133  
   1.134  
   1.135 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
   1.136 -      (x, AList.lookup (op =) parms x, mx)) fixes)
   1.137 +fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
   1.138 +      let val x = Name.name_of binding
   1.139 +      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   1.140    | finish_ext_elem parms _ (Constrains _, _) = Constrains []
   1.141    | finish_ext_elem _ close (Assumes asms, propp) =
   1.142        close (Assumes (map #1 asms ~~ propp))
   1.143 @@ -1274,7 +1275,7 @@
   1.144      list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
   1.145        Term.fast_term_ord (d1, d2)) (defs1, defs2);
   1.146  structure Defstab =
   1.147 -    TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
   1.148 +    TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
   1.149          val ord = defs_ord);
   1.150  
   1.151  fun rem_dup_defs es ds =
   1.152 @@ -1387,7 +1388,7 @@
   1.153        |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
   1.154    | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
   1.155       {var = I, typ = I, term = I,
   1.156 -      name = prep_name,
   1.157 +      name = Name.map_name prep_name,
   1.158        fact = get ctxt,
   1.159        attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
   1.160  
   1.161 @@ -1572,8 +1573,8 @@
   1.162  (* naming of interpreted theorems *)
   1.163  
   1.164  fun add_param_prefixss s =
   1.165 -  (map o apfst o apfst) (NameSpace.qualified s);
   1.166 -fun drop_param_prefixss args = (map o apfst o apfst)
   1.167 +  (map o apfst o apfst o Name.map_name) (NameSpace.qualified s);
   1.168 +fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
   1.169    (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
   1.170  
   1.171  fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
   1.172 @@ -1660,7 +1661,7 @@
   1.173  
   1.174  fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
   1.175    let
   1.176 -    val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
   1.177 +    val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
   1.178  (* need to add parameter prefix *) (* FIXME *)
   1.179        Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   1.180        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   1.181 @@ -1724,7 +1725,7 @@
   1.182      (fn (axiom, elems, params, decls, regs, intros, dests) =>
   1.183        (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
   1.184    add_thmss loc Thm.internalK
   1.185 -    [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   1.186 +    [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   1.187  
   1.188  in
   1.189  
   1.190 @@ -1864,12 +1865,13 @@
   1.191              thy
   1.192              |> def_pred aname parms defs exts exts';
   1.193            val elemss' = change_assumes_elemss axioms elemss;
   1.194 -          val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
   1.195 +          val a_elem = [(("", []),
   1.196 +            [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
   1.197            val (_, thy'') =
   1.198              thy'
   1.199              |> Sign.add_path aname
   1.200              |> Sign.no_base_names
   1.201 -            |> PureThy.note_thmss Thm.internalK [((introN, []), [([intro], [])])]
   1.202 +            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
   1.203              ||> Sign.restore_naming thy';
   1.204          in ((elemss', [statement]), a_elem, [intro], thy'') end;
   1.205      val (predicate, stmt', elemss'', b_intro, thy'''') =
   1.206 @@ -1882,14 +1884,15 @@
   1.207            val cstatement = Thm.cterm_of thy''' statement;
   1.208            val elemss'' = change_elemss_hyps axioms elemss';
   1.209            val b_elem = [(("", []),
   1.210 -               [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
   1.211 +               [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
   1.212            val (_, thy'''') =
   1.213              thy'''
   1.214              |> Sign.add_path pname
   1.215              |> Sign.no_base_names
   1.216              |> PureThy.note_thmss Thm.internalK
   1.217 -                 [((introN, []), [([intro], [])]),
   1.218 -                  ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   1.219 +                 [((Name.binding introN, []), [([intro], [])]),
   1.220 +                  ((Name.binding axiomsN, []),
   1.221 +                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   1.222              ||> Sign.restore_naming thy''';
   1.223          in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
   1.224    in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
   1.225 @@ -1905,7 +1908,7 @@
   1.226  
   1.227  fun defines_to_notes is_ext thy (Defines defs) defns =
   1.228      let
   1.229 -      val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
   1.230 +      val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
   1.231        val notes = map (fn (a, (def, _)) =>
   1.232          (a, [([assume (cterm_of thy def)], [])])) defs
   1.233      in
   1.234 @@ -1994,9 +1997,9 @@
   1.235  end;
   1.236  
   1.237  val _ = Context.>> (Context.map_theory
   1.238 - (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
   1.239 + (add_locale_i "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
   1.240    snd #> ProofContext.theory_of #>
   1.241 -  add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
   1.242 +  add_locale_i "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
   1.243    snd #> ProofContext.theory_of));
   1.244  
   1.245  
   1.246 @@ -2374,7 +2377,7 @@
   1.247              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
   1.248                  let
   1.249                    val att_morphism =
   1.250 -                    Morphism.name_morphism (NameSpace.qualified prfx) $>
   1.251 +                    Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
   1.252                      Morphism.thm_morphism satisfy $>
   1.253                      Element.inst_morphism thy insts $>
   1.254                      Morphism.thm_morphism disch;
   1.255 @@ -2435,7 +2438,7 @@
   1.256    in
   1.257      state
   1.258      |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
   1.259 -      "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
   1.260 +      "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
   1.261      |> Element.refine_witness |> Seq.hd
   1.262    end;
   1.263