src/Pure/Isar/locale.ML
changeset 30764 3e3e7aa0cc7a
parent 30763 6976521b4263
child 30773 6cc9964436c3
     1.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:53:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 20:25:23 2009 +0100
     1.3 @@ -56,10 +56,8 @@
     1.4    val add_dependency: string -> string * morphism -> theory -> theory
     1.5  
     1.6    (* Activation *)
     1.7 -  val activate_declarations: theory -> string * morphism ->
     1.8 -    Proof.context -> Proof.context
     1.9 -  val activate_global_facts: string * morphism -> theory -> theory
    1.10 -  val activate_local_facts: string * morphism -> Proof.context -> Proof.context
    1.11 +  val activate_declarations: string * morphism -> Proof.context -> Proof.context
    1.12 +  val activate_facts: string * morphism -> Context.generic -> Context.generic
    1.13    val init: string -> theory -> Proof.context
    1.14  
    1.15    (* Reasoning about locales *)
    1.16 @@ -194,8 +192,6 @@
    1.17    fun merge _ = ToDo;
    1.18  );
    1.19  
    1.20 -in
    1.21 -
    1.22  fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
    1.23    | finish _ (Ready ids) = ids;
    1.24  
    1.25 @@ -204,13 +200,10 @@
    1.26      Ready _ => NONE
    1.27    | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
    1.28  
    1.29 -fun get_global_idents thy =
    1.30 -  let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
    1.31 -val put_global_idents = Context.theory_map o Identifiers.put o Ready;
    1.32 +in
    1.33  
    1.34 -fun get_local_idents ctxt =
    1.35 -  let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
    1.36 -val put_local_idents = Context.proof_map o Identifiers.put o Ready;
    1.37 +val get_idents = (fn Ready ids => ids) o Identifiers.get;
    1.38 +val put_idents = Identifiers.put o Ready;
    1.39  
    1.40  end;
    1.41  
    1.42 @@ -260,12 +253,14 @@
    1.43  
    1.44  (* Declarations, facts and entire locale content *)
    1.45  
    1.46 -fun activate_decls thy (name, morph) ctxt =
    1.47 +fun activate_decls (name, morph) context =
    1.48    let
    1.49 +    val thy = Context.theory_of context;
    1.50      val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
    1.51    in
    1.52 -    ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
    1.53 -      fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
    1.54 +    context
    1.55 +    |> fold_rev (fn (decl, _) => decl morph) typ_decls
    1.56 +    |> fold_rev (fn (decl, _) => decl morph) term_decls
    1.57    end;
    1.58  
    1.59  fun activate_notes activ_elem transfer thy (name, morph) input =
    1.60 @@ -281,18 +276,17 @@
    1.61  
    1.62  fun activate_all name thy activ_elem transfer (marked, input) =
    1.63    let
    1.64 -    val {parameters = (_, params), spec = (asm, defs), ...} =
    1.65 -      the_locale thy name;
    1.66 -  in
    1.67 -    input |>
    1.68 +    val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
    1.69 +    val input' = input |>
    1.70        (not (null params) ?
    1.71          activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
    1.72        (* FIXME type parameters *)
    1.73 -      (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
    1.74 +      (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
    1.75        (if not (null defs)
    1.76          then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
    1.77 -        else I) |>
    1.78 -      pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
    1.79 +        else I);
    1.80 +  in
    1.81 +    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
    1.82    end;
    1.83  
    1.84  
    1.85 @@ -300,64 +294,65 @@
    1.86  
    1.87  local
    1.88  
    1.89 -fun init_global_elem (Notes (kind, facts)) thy =
    1.90 -  let
    1.91 -    val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
    1.92 -  in PureThy.note_thmss kind facts' thy |> snd end
    1.93 -
    1.94 -fun init_local_elem (Fixes fixes) ctxt = ctxt |>
    1.95 -      ProofContext.add_fixes fixes |> snd
    1.96 -  | init_local_elem (Assumes assms) ctxt =
    1.97 +fun init_elem (Fixes fixes) (Context.Proof ctxt) =
    1.98 +      Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
    1.99 +  | init_elem (Assumes assms) (Context.Proof ctxt) =
   1.100        let
   1.101 -        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
   1.102 -      in
   1.103 -        ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
   1.104 -          ProofContext.add_assms_i Assumption.assume_export assms' |> snd
   1.105 -     end
   1.106 -  | init_local_elem (Defines defs) ctxt =
   1.107 +        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
   1.108 +        val ctxt' = ctxt
   1.109 +          |> fold Variable.auto_fixes (maps (map fst o snd) assms')
   1.110 +          |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
   1.111 +      in Context.Proof ctxt' end
   1.112 +  | init_elem (Defines defs) (Context.Proof ctxt) =
   1.113        let
   1.114 -        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
   1.115 -      in
   1.116 -        ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
   1.117 -          ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
   1.118 -          snd
   1.119 -      end
   1.120 -  | init_local_elem (Notes (kind, facts)) ctxt =
   1.121 +        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   1.122 +        val ctxt' = ctxt
   1.123 +          |> fold Variable.auto_fixes (map (fst o snd) defs')
   1.124 +          |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
   1.125 +          |> snd;
   1.126 +      in Context.Proof ctxt' end
   1.127 +  | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
   1.128        let
   1.129          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
   1.130 -      in ProofContext.note_thmss kind facts' ctxt |> snd end
   1.131 -
   1.132 -fun cons_elem false (Notes notes) elems = elems
   1.133 -  | cons_elem _ elem elems = elem :: elems
   1.134 +      in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
   1.135 +  | init_elem (Notes (kind, facts)) (Context.Theory thy) =
   1.136 +      let
   1.137 +        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
   1.138 +      in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
   1.139 +  | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
   1.140  
   1.141  in
   1.142  
   1.143 -fun activate_declarations thy dep ctxt =
   1.144 -  roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
   1.145 +fun activate_declarations dep ctxt =
   1.146 +  let
   1.147 +    val context = Context.Proof ctxt;
   1.148 +    val thy = Context.theory_of context;
   1.149 +    val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
   1.150 +  in Context.the_proof context' end;
   1.151  
   1.152 -fun activate_global_facts dep thy =
   1.153 -  roundup thy (activate_notes init_global_elem Element.transfer_morphism)
   1.154 -    dep (get_global_idents thy, thy) |-> put_global_idents;
   1.155 -
   1.156 -fun activate_local_facts dep ctxt =
   1.157 -  roundup (ProofContext.theory_of ctxt)
   1.158 -  (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
   1.159 -    (get_local_idents ctxt, ctxt) |-> put_local_idents;
   1.160 +fun activate_facts dep context =
   1.161 +  let
   1.162 +    val thy = Context.theory_of context;
   1.163 +    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
   1.164 +  in roundup thy activate dep (get_idents context, context) |-> put_idents end;
   1.165  
   1.166  fun init name thy =
   1.167 -  activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
   1.168 -    ([], ProofContext.init thy) |-> put_local_idents;
   1.169 +  activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
   1.170 +    ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
   1.171  
   1.172 -fun print_locale thy show_facts name =
   1.173 +fun print_locale thy show_facts raw_name =
   1.174    let
   1.175 -    val name' = intern thy name;
   1.176 -    val ctxt = init name' thy
   1.177 +    val name = intern thy raw_name;
   1.178 +    val ctxt = init name thy;
   1.179 +    fun cons_elem (elem as Notes _) = show_facts ? cons elem
   1.180 +      | cons_elem elem = cons elem;
   1.181 +    val elems =
   1.182 +      activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
   1.183 +      |> snd |> rev;
   1.184    in
   1.185 -    Pretty.big_list "locale elements:"
   1.186 -      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
   1.187 -        ([], []) |> snd |> rev |>
   1.188 -        map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   1.189 -  end
   1.190 +    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
   1.191 +    |> Pretty.writeln
   1.192 +  end;
   1.193  
   1.194  end;
   1.195  
   1.196 @@ -377,24 +372,25 @@
   1.197  );
   1.198  
   1.199  val get_registrations =
   1.200 -  Registrations.get #> map fst #> map (apsnd op $>);
   1.201 +  Registrations.get #> map (#1 #> apsnd op $>);
   1.202  
   1.203  fun add_registration (name, (base_morph, export)) thy =
   1.204    roundup thy (fn _ => fn (name', morph') =>
   1.205 -    (Registrations.map o cons) ((name', (morph', export)), stamp ()))
   1.206 -    (name, base_morph) (get_global_idents thy, thy) |> snd
   1.207 -    (* FIXME |-> put_global_idents ?*);
   1.208 +    Registrations.map (cons ((name', (morph', export)), stamp ())))
   1.209 +    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
   1.210 +    (* FIXME |-> put_global_idents ?*)
   1.211  
   1.212  fun amend_registration morph (name, base_morph) thy =
   1.213    let
   1.214 -    val regs = (Registrations.get #> map fst) thy;
   1.215 +    val regs = map #1 (Registrations.get thy);
   1.216      val base = instance_of thy name base_morph;
   1.217      fun match (name', (morph', _)) =
   1.218        name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
   1.219      val i = find_index match (rev regs);
   1.220 -    val _ = if i = ~1 then error ("No registration of locale " ^
   1.221 +    val _ =
   1.222 +      if i = ~1 then error ("No registration of locale " ^
   1.223          quote (extern thy name) ^ " and parameter instantiation " ^
   1.224 -        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
   1.225 +        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
   1.226        else ();
   1.227    in
   1.228      Registrations.map (nth_map (length regs - 1 - i)