simplified Locale.activate operations, using generic context;
authorwenzelm
Sat Mar 28 20:25:23 2009 +0100 (2009-03-28)
changeset 307643e3e7aa0cc7a
parent 30763 6976521b4263
child 30772 dca52e229138
simplified Locale.activate operations, using generic context;
misc tuning;
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sat Mar 28 17:53:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Mar 28 20:25:23 2009 +0100
     1.3 @@ -285,7 +285,7 @@
     1.4         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     1.5      #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
     1.6         Locale.add_registration (class, (morph, export_morph))
     1.7 -    #> Locale.activate_global_facts (class, morph $> export_morph)
     1.8 +    #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
     1.9      #> register class sups params base_sort base_morph axiom assm_intro of_class))
    1.10      |> TheoryTarget.init (SOME class)
    1.11      |> pair class
     2.1 --- a/src/Pure/Isar/class_target.ML	Sat Mar 28 17:53:33 2009 +0100
     2.2 +++ b/src/Pure/Isar/class_target.ML	Sat Mar 28 20:25:23 2009 +0100
     2.3 @@ -287,8 +287,8 @@
     2.4      |> fold (fn dep_morph => Locale.add_dependency sub (sup,
     2.5          dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
     2.6            (the_list some_dep_morph)
     2.7 -    |> (fn thy => fold_rev Locale.activate_global_facts
     2.8 -      (Locale.get_registrations thy) thy)
     2.9 +    |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    2.10 +        (Locale.get_registrations thy) thy)
    2.11    end;
    2.12  
    2.13  
     3.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 28 17:53:33 2009 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 28 20:25:23 2009 +0100
     3.3 @@ -352,7 +352,7 @@
     3.4          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
     3.5          val inst''' = insts'' |> List.last |> snd |> snd;
     3.6          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
     3.7 -        val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
     3.8 +        val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
     3.9        in (i + 1, insts', ctxt'') end;
    3.10  
    3.11      fun prep_elem insts raw_elem (elems, ctxt) =
    3.12 @@ -437,7 +437,7 @@
    3.13      (* Declare parameters and imported facts *)
    3.14      val context' = context |>
    3.15        fix_params fixed |>
    3.16 -      fold Locale.activate_local_facts deps;
    3.17 +      fold (Context.proof_map o Locale.activate_facts) deps;
    3.18      val (elems', _) = context' |>
    3.19        ProofContext.set_stmt true |>
    3.20        activate elems;
    3.21 @@ -787,7 +787,7 @@
    3.22      fun after_qed witss = ProofContext.theory
    3.23        (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
    3.24          (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
    3.25 -      (fn thy => fold_rev Locale.activate_global_facts
    3.26 +      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
    3.27          (Locale.get_registrations thy) thy));
    3.28    in Element.witness_proof after_qed propss goal_ctxt end;
    3.29  
    3.30 @@ -827,7 +827,7 @@
    3.31      fun store_eqns_activate regs [] thy =
    3.32            thy
    3.33            |> fold (fn (name, morph) =>
    3.34 -               Locale.activate_global_facts (name, morph $> export)) regs
    3.35 +               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
    3.36        | store_eqns_activate regs eqs thy =
    3.37            let
    3.38              val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
    3.39 @@ -839,7 +839,7 @@
    3.40              thy
    3.41              |> fold (fn (name, morph) =>
    3.42                  Locale.amend_registration eq_morph (name, morph) #>
    3.43 -                Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
    3.44 +                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
    3.45              |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
    3.46              |> snd
    3.47            end;
    3.48 @@ -873,7 +873,7 @@
    3.49      fun store_reg (name, morph) thms =
    3.50        let
    3.51          val morph' = morph $> Element.satisfy_morphism thms $> export;
    3.52 -      in Locale.activate_local_facts (name, morph') end;
    3.53 +      in Context.proof_map (Locale.activate_facts (name, morph')) end;
    3.54  
    3.55      fun after_qed wits =
    3.56        Proof.map_context (fold2 store_reg regs wits);
     4.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:53:33 2009 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 20:25:23 2009 +0100
     4.3 @@ -56,10 +56,8 @@
     4.4    val add_dependency: string -> string * morphism -> theory -> theory
     4.5  
     4.6    (* Activation *)
     4.7 -  val activate_declarations: theory -> string * morphism ->
     4.8 -    Proof.context -> Proof.context
     4.9 -  val activate_global_facts: string * morphism -> theory -> theory
    4.10 -  val activate_local_facts: string * morphism -> Proof.context -> Proof.context
    4.11 +  val activate_declarations: string * morphism -> Proof.context -> Proof.context
    4.12 +  val activate_facts: string * morphism -> Context.generic -> Context.generic
    4.13    val init: string -> theory -> Proof.context
    4.14  
    4.15    (* Reasoning about locales *)
    4.16 @@ -194,8 +192,6 @@
    4.17    fun merge _ = ToDo;
    4.18  );
    4.19  
    4.20 -in
    4.21 -
    4.22  fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
    4.23    | finish _ (Ready ids) = ids;
    4.24  
    4.25 @@ -204,13 +200,10 @@
    4.26      Ready _ => NONE
    4.27    | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
    4.28  
    4.29 -fun get_global_idents thy =
    4.30 -  let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
    4.31 -val put_global_idents = Context.theory_map o Identifiers.put o Ready;
    4.32 +in
    4.33  
    4.34 -fun get_local_idents ctxt =
    4.35 -  let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
    4.36 -val put_local_idents = Context.proof_map o Identifiers.put o Ready;
    4.37 +val get_idents = (fn Ready ids => ids) o Identifiers.get;
    4.38 +val put_idents = Identifiers.put o Ready;
    4.39  
    4.40  end;
    4.41  
    4.42 @@ -260,12 +253,14 @@
    4.43  
    4.44  (* Declarations, facts and entire locale content *)
    4.45  
    4.46 -fun activate_decls thy (name, morph) ctxt =
    4.47 +fun activate_decls (name, morph) context =
    4.48    let
    4.49 +    val thy = Context.theory_of context;
    4.50      val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
    4.51    in
    4.52 -    ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
    4.53 -      fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
    4.54 +    context
    4.55 +    |> fold_rev (fn (decl, _) => decl morph) typ_decls
    4.56 +    |> fold_rev (fn (decl, _) => decl morph) term_decls
    4.57    end;
    4.58  
    4.59  fun activate_notes activ_elem transfer thy (name, morph) input =
    4.60 @@ -281,18 +276,17 @@
    4.61  
    4.62  fun activate_all name thy activ_elem transfer (marked, input) =
    4.63    let
    4.64 -    val {parameters = (_, params), spec = (asm, defs), ...} =
    4.65 -      the_locale thy name;
    4.66 -  in
    4.67 -    input |>
    4.68 +    val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
    4.69 +    val input' = input |>
    4.70        (not (null params) ?
    4.71          activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
    4.72        (* FIXME type parameters *)
    4.73 -      (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
    4.74 +      (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
    4.75        (if not (null defs)
    4.76          then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
    4.77 -        else I) |>
    4.78 -      pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
    4.79 +        else I);
    4.80 +  in
    4.81 +    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
    4.82    end;
    4.83  
    4.84  
    4.85 @@ -300,64 +294,65 @@
    4.86  
    4.87  local
    4.88  
    4.89 -fun init_global_elem (Notes (kind, facts)) thy =
    4.90 -  let
    4.91 -    val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    4.92 -  in PureThy.note_thmss kind facts' thy |> snd end
    4.93 -
    4.94 -fun init_local_elem (Fixes fixes) ctxt = ctxt |>
    4.95 -      ProofContext.add_fixes fixes |> snd
    4.96 -  | init_local_elem (Assumes assms) ctxt =
    4.97 +fun init_elem (Fixes fixes) (Context.Proof ctxt) =
    4.98 +      Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
    4.99 +  | init_elem (Assumes assms) (Context.Proof ctxt) =
   4.100        let
   4.101 -        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
   4.102 -      in
   4.103 -        ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
   4.104 -          ProofContext.add_assms_i Assumption.assume_export assms' |> snd
   4.105 -     end
   4.106 -  | init_local_elem (Defines defs) ctxt =
   4.107 +        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
   4.108 +        val ctxt' = ctxt
   4.109 +          |> fold Variable.auto_fixes (maps (map fst o snd) assms')
   4.110 +          |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
   4.111 +      in Context.Proof ctxt' end
   4.112 +  | init_elem (Defines defs) (Context.Proof ctxt) =
   4.113        let
   4.114 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
   4.115 -      in
   4.116 -        ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
   4.117 -          ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
   4.118 -          snd
   4.119 -      end
   4.120 -  | init_local_elem (Notes (kind, facts)) ctxt =
   4.121 +        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   4.122 +        val ctxt' = ctxt
   4.123 +          |> fold Variable.auto_fixes (map (fst o snd) defs')
   4.124 +          |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
   4.125 +          |> snd;
   4.126 +      in Context.Proof ctxt' end
   4.127 +  | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
   4.128        let
   4.129          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   4.130 -      in ProofContext.note_thmss kind facts' ctxt |> snd end
   4.131 -
   4.132 -fun cons_elem false (Notes notes) elems = elems
   4.133 -  | cons_elem _ elem elems = elem :: elems
   4.134 +      in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
   4.135 +  | init_elem (Notes (kind, facts)) (Context.Theory thy) =
   4.136 +      let
   4.137 +        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   4.138 +      in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
   4.139 +  | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
   4.140  
   4.141  in
   4.142  
   4.143 -fun activate_declarations thy dep ctxt =
   4.144 -  roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
   4.145 +fun activate_declarations dep ctxt =
   4.146 +  let
   4.147 +    val context = Context.Proof ctxt;
   4.148 +    val thy = Context.theory_of context;
   4.149 +    val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
   4.150 +  in Context.the_proof context' end;
   4.151  
   4.152 -fun activate_global_facts dep thy =
   4.153 -  roundup thy (activate_notes init_global_elem Element.transfer_morphism)
   4.154 -    dep (get_global_idents thy, thy) |-> put_global_idents;
   4.155 -
   4.156 -fun activate_local_facts dep ctxt =
   4.157 -  roundup (ProofContext.theory_of ctxt)
   4.158 -  (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
   4.159 -    (get_local_idents ctxt, ctxt) |-> put_local_idents;
   4.160 +fun activate_facts dep context =
   4.161 +  let
   4.162 +    val thy = Context.theory_of context;
   4.163 +    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
   4.164 +  in roundup thy activate dep (get_idents context, context) |-> put_idents end;
   4.165  
   4.166  fun init name thy =
   4.167 -  activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
   4.168 -    ([], ProofContext.init thy) |-> put_local_idents;
   4.169 +  activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
   4.170 +    ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
   4.171  
   4.172 -fun print_locale thy show_facts name =
   4.173 +fun print_locale thy show_facts raw_name =
   4.174    let
   4.175 -    val name' = intern thy name;
   4.176 -    val ctxt = init name' thy
   4.177 +    val name = intern thy raw_name;
   4.178 +    val ctxt = init name thy;
   4.179 +    fun cons_elem (elem as Notes _) = show_facts ? cons elem
   4.180 +      | cons_elem elem = cons elem;
   4.181 +    val elems =
   4.182 +      activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   4.183 +      |> snd |> rev;
   4.184    in
   4.185 -    Pretty.big_list "locale elements:"
   4.186 -      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   4.187 -        ([], []) |> snd |> rev |>
   4.188 -        map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   4.189 -  end
   4.190 +    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   4.191 +    |> Pretty.writeln
   4.192 +  end;
   4.193  
   4.194  end;
   4.195  
   4.196 @@ -377,24 +372,25 @@
   4.197  );
   4.198  
   4.199  val get_registrations =
   4.200 -  Registrations.get #> map fst #> map (apsnd op $>);
   4.201 +  Registrations.get #> map (#1 #> apsnd op $>);
   4.202  
   4.203  fun add_registration (name, (base_morph, export)) thy =
   4.204    roundup thy (fn _ => fn (name', morph') =>
   4.205 -    (Registrations.map o cons) ((name', (morph', export)), stamp ()))
   4.206 -    (name, base_morph) (get_global_idents thy, thy) |> snd
   4.207 -    (* FIXME |-> put_global_idents ?*);
   4.208 +    Registrations.map (cons ((name', (morph', export)), stamp ())))
   4.209 +    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
   4.210 +    (* FIXME |-> put_global_idents ?*)
   4.211  
   4.212  fun amend_registration morph (name, base_morph) thy =
   4.213    let
   4.214 -    val regs = (Registrations.get #> map fst) thy;
   4.215 +    val regs = map #1 (Registrations.get thy);
   4.216      val base = instance_of thy name base_morph;
   4.217      fun match (name', (morph', _)) =
   4.218        name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   4.219      val i = find_index match (rev regs);
   4.220 -    val _ = if i = ~1 then error ("No registration of locale " ^
   4.221 +    val _ =
   4.222 +      if i = ~1 then error ("No registration of locale " ^
   4.223          quote (extern thy name) ^ " and parameter instantiation " ^
   4.224 -        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   4.225 +        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   4.226        else ();
   4.227    in
   4.228      Registrations.map (nth_map (length regs - 1 - i)