src/Pure/Isar/locale.ML
changeset 27716 96699d8eb49e
parent 27709 2ba55d217705
child 27761 b95e9ba0ca1d
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Aug 01 12:57:50 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Aug 01 17:41:37 2008 +0200
     1.3 @@ -58,8 +58,11 @@
     1.4      ((string * Attrib.src list) * term list) list
     1.5    val global_asms_of: theory -> string ->
     1.6      ((string * Attrib.src list) * term list) list
     1.7 +
     1.8 +  (* Theorems *)
     1.9    val intros: theory -> string -> thm list * thm list
    1.10    val dests: theory -> string -> thm list
    1.11 +  (* Not part of the official interface.  DO NOT USE *)
    1.12    val facts_of: theory -> string
    1.13      -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list list
    1.14  
    1.15 @@ -155,11 +158,9 @@
    1.16      (* For locales that define predicates this is [A [A]], where A is the locale
    1.17         specification.  Otherwise [].
    1.18         Only required to generate the right witnesses for locales with predicates. *)
    1.19 -  imports: expr,                                                     (*dynamic imports*)
    1.20    elems: (Element.context_i * stamp) list,
    1.21      (* Static content, neither Fixes nor Constrains elements *)
    1.22    params: ((string * typ) * mixfix) list,                             (*all params*)
    1.23 -  lparams: string list,                                             (*local params*)
    1.24    decls: decl list * decl list,                    (*type/term_syntax declarations*)
    1.25    regs: ((string * string list) * Element.witness list) list,
    1.26      (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
    1.27 @@ -352,13 +353,11 @@
    1.28    val extend = I;
    1.29  
    1.30    fun join_locales _
    1.31 -    ({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros, dests}: locale,
    1.32 +    ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
    1.33        {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
    1.34       {axiom = axiom,
    1.35 -      imports = imports,
    1.36        elems = merge_lists (eq_snd (op =)) elems elems',
    1.37        params = params,
    1.38 -      lparams = lparams,
    1.39        decls =
    1.40         (Library.merge (eq_snd (op =)) (decls1, decls1'),
    1.41          Library.merge (eq_snd (op =)) (decls2, decls2')),
    1.42 @@ -399,14 +398,14 @@
    1.43  
    1.44  fun change_locale name f thy =
    1.45    let
    1.46 -    val {axiom, imports, elems, params, lparams, decls, regs, intros, dests} =
    1.47 +    val {axiom, elems, params, decls, regs, intros, dests} =
    1.48          the_locale thy name;
    1.49 -    val (axiom', imports', elems', params', lparams', decls', regs', intros', dests') =
    1.50 -      f (axiom, imports, elems, params, lparams, decls, regs, intros, dests);
    1.51 +    val (axiom', elems', params', decls', regs', intros', dests') =
    1.52 +      f (axiom, elems, params, decls, regs, intros, dests);
    1.53    in
    1.54      thy
    1.55      |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
    1.56 -          imports = imports', elems = elems', params = params', lparams = lparams',
    1.57 +          elems = elems', params = params',
    1.58            decls = decls', regs = regs', intros = intros', dests = dests'}))
    1.59    end;
    1.60  
    1.61 @@ -471,8 +470,8 @@
    1.62  
    1.63  
    1.64  fun put_registration_in_locale name id =
    1.65 -  change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
    1.66 -    (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros, dests));
    1.67 +  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
    1.68 +    (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
    1.69  
    1.70  
    1.71  (* add witness theorem to registration, ignored if registration not present *)
    1.72 @@ -485,11 +484,11 @@
    1.73  
    1.74  
    1.75  fun add_witness_in_locale name id thm =
    1.76 -  change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
    1.77 +  change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
    1.78      let
    1.79        fun add (id', thms) =
    1.80          if id = id' then (id', thm :: thms) else (id', thms);
    1.81 -    in (axiom, imports, elems, params, lparams, decls, map add regs, intros, dests) end);
    1.82 +    in (axiom, elems, params, decls, map add regs, intros, dests) end);
    1.83  
    1.84  
    1.85  (* add equation to registration, ignored if registration not present *)
    1.86 @@ -733,13 +732,9 @@
    1.87  
    1.88      fun params_of (expr as Locale name) =
    1.89            let
    1.90 -            val {imports, params, ...} = the_locale thy name;
    1.91 -            val parms = map (fst o fst) params;
    1.92 -            val (parms', types', syn') = params_of imports;
    1.93 -            val all_parms = merge_lists (op =) parms' parms;
    1.94 -            val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
    1.95 -            val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
    1.96 -          in (all_parms, all_types, all_syn) end
    1.97 +            val {params, ...} = the_locale thy name;
    1.98 +          in (map (fst o fst) params, params |> map fst |> Symtab.make,
    1.99 +               params |> map (apfst fst) |> Symtab.make) end
   1.100        | params_of (expr as Rename (e, xs)) =
   1.101            let
   1.102              val (parms', types', syn') = params_of e;
   1.103 @@ -814,7 +809,7 @@
   1.104                 map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
   1.105           else (parms, mode));
   1.106  
   1.107 -    (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
   1.108 +    (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
   1.109  
   1.110      fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
   1.111          if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
   1.112 @@ -876,14 +871,11 @@
   1.113         identify at top level (top = true);
   1.114         parms is accumulated list of parameters *)
   1.115            let
   1.116 -            val {axiom, imports, params, ...} = the_locale thy name;
   1.117 +            val {axiom, params, ...} = the_locale thy name;
   1.118              val ps = map (#1 o #1) params;
   1.119 -            val (ids', parms') = identify false imports;
   1.120 -                (* acyclic import dependencies *)
   1.121 -
   1.122 -            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
   1.123 +            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
   1.124              val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
   1.125 -            in (ids_ax, merge_lists (op =) parms' ps) end
   1.126 +            in (ids_ax, ps) end
   1.127        | identify top (Rename (e, xs)) =
   1.128            let
   1.129              val (ids', parms') = identify top e;
   1.130 @@ -1692,9 +1684,9 @@
   1.131          [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
   1.132      val ctxt'' = ctxt' |> ProofContext.theory
   1.133        (change_locale loc
   1.134 -        (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
   1.135 -          (axiom, imports, elems @ [(Notes args', stamp ())],
   1.136 -            params, lparams, decls, regs, intros, dests))
   1.137 +        (fn (axiom, elems, params, decls, regs, intros, dests) =>
   1.138 +          (axiom, elems @ [(Notes args', stamp ())],
   1.139 +            params, decls, regs, intros, dests))
   1.140        #> note_thmss_registrations loc args');
   1.141    in ctxt'' end;
   1.142  
   1.143 @@ -1707,8 +1699,8 @@
   1.144  
   1.145  fun add_decls add loc decl =
   1.146    ProofContext.theory (change_locale loc
   1.147 -    (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
   1.148 -      (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros, dests))) #>
   1.149 +    (fn (axiom, elems, params, decls, regs, intros, dests) =>
   1.150 +      (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
   1.151    add_thmss loc Thm.internalK
   1.152      [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   1.153  
   1.154 @@ -1922,7 +1914,6 @@
   1.155          prep_ctxt raw_imports raw_body thy_ctxt;
   1.156      val elemss = import_elemss @ body_elemss |>
   1.157        map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
   1.158 -    val imports = prep_expr thy raw_imports;
   1.159  
   1.160      val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
   1.161        List.foldr Term.add_typ_tfrees [] (map snd parms);
   1.162 @@ -1964,10 +1955,8 @@
   1.163        |> PureThy.note_thmss Thm.assumptionK facts' |> snd
   1.164        |> Sign.restore_naming thy'
   1.165        |> register_locale name {axiom = axs',
   1.166 -        imports = empty,
   1.167          elems = map (fn e => (e, stamp ())) elems'',
   1.168          params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
   1.169 -        lparams = map #1 (params_of' body_elemss),
   1.170          decls = ([], []),
   1.171          regs = regs,
   1.172          intros = intros,