tuned for uniformity
authorhaftmann
Sun Apr 21 10:41:18 2013 +0200 (2013-04-21)
changeset 51727cf97bb5bbc90
parent 51726 b3e599b5ecc8
child 51728 0f6e8c4144a5
tuned for uniformity
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.3 @@ -819,22 +819,28 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun note_eqns_register deps witss attrss eqns export export' =
     1.8 -  Attrib.generic_notes Thm.lemmaK
     1.9 -    (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.10 -  #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
    1.11 -  #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.12 -    fn context =>
    1.13 +fun note_eqns_register deps witss attrss eqns export export' context =
    1.14 +  let
    1.15 +    val facts = 
    1.16 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.17 +    val (eqns', context') = context 
    1.18 +      |> Attrib.generic_notes Thm.lemmaK facts
    1.19 +      |-> (fn facts' => `(fn context'' => meta_rewrite (Context.proof_of context'') (maps snd facts')));
    1.20 +  in
    1.21 +    context'
    1.22 +    |> fold2 (fn (dep, morph) => fn wits => fn context'' =>
    1.23        Locale.add_registration
    1.24          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.25 -        (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
    1.26 -        export context) (deps ~~ witss));
    1.27 +        (Element.eq_morphism (Context.theory_of context'') eqns' |> Option.map (rpair true))
    1.28 +        export context'') deps witss
    1.29 +  end;
    1.30  
    1.31  fun gen_interpretation prep_expr parse_prop prep_attr
    1.32      expression equations thy =
    1.33    let
    1.34 -    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global thy
    1.35 -      |> prep_expr expression;
    1.36 +    val initial_ctxt = Proof_Context.init_global thy;
    1.37 +
    1.38 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.39      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.40  
    1.41      val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.42 @@ -891,27 +897,27 @@
    1.43    let
    1.44      val facts =
    1.45        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.46 -    val eqns' = ctxt
    1.47 +    val (eqns', _) = ctxt (* FIXME duplication to add_thmss *)
    1.48        |> Attrib.local_notes Thm.lemmaK facts
    1.49 -      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
    1.50 -      |> fst;  (* FIXME duplication to add_thmss *)
    1.51 +      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
    1.52    in
    1.53      ctxt
    1.54      |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
    1.55 -    |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
    1.56 +    |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits =>
    1.57        fn thy =>
    1.58          Locale.add_dependency target
    1.59            (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.60            (Element.eq_morphism thy eqns' |> Option.map (rpair true))
    1.61 -          export thy) (deps ~~ witss))
    1.62 +          export thy) deps witss)
    1.63    end;
    1.64  
    1.65  fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
    1.66      before_exit raw_target expression equations thy =
    1.67    let
    1.68      val target = prep_loc thy raw_target;
    1.69 -    val target_ctxt = Named_Target.init before_exit target thy;
    1.70 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.71 +    val initial_ctxt = Named_Target.init before_exit target thy;
    1.72 +
    1.73 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.74      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.75  
    1.76      val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
     2.1 --- a/src/Pure/Isar/locale.ML	Sun Apr 21 10:41:18 2013 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Sun Apr 21 10:41:18 2013 +0200
     2.3 @@ -458,14 +458,15 @@
     2.4      val thy = Context.theory_of context;
     2.5      val regs = Registrations.get context |> fst;
     2.6      val base = instance_of thy name (morph $> export);
     2.7 +    val serial' = case Idtab.lookup regs (name, base) of
     2.8 +        NONE =>
     2.9 +          error ("No interpretation of locale " ^
    2.10 +            quote (extern thy name) ^ " with\nparameter instantiation " ^
    2.11 +            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    2.12 +            " available")
    2.13 +      | SOME (_, serial') => serial';
    2.14    in
    2.15 -    (case Idtab.lookup regs (name, base) of
    2.16 -      NONE =>
    2.17 -        error ("No interpretation of locale " ^
    2.18 -          quote (extern thy name) ^ " with\nparameter instantiation " ^
    2.19 -          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    2.20 -          " available")
    2.21 -    | SOME (_, serial') => add_mixin serial' mixin context)
    2.22 +    add_mixin serial' mixin context
    2.23    end;
    2.24  
    2.25  (* Note that a registration that would be subsumed by an existing one will not be
    2.26 @@ -477,13 +478,15 @@
    2.27      val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
    2.28      val morph = base_morph $> mix;
    2.29      val inst = instance_of thy name morph;
    2.30 +    val idents = Idents.get context;
    2.31    in
    2.32 -    if redundant_ident thy (Idents.get context) (name, inst)
    2.33 +    if redundant_ident thy idents (name, inst)
    2.34      then context  (* FIXME amend mixins? *)
    2.35      else
    2.36 -      (Idents.get context, context)
    2.37 +      (idents, context)
    2.38        (* add new registrations with inherited mixins *)
    2.39 -      |> (snd o roundup thy (add_reg thy export) export (name, morph))
    2.40 +      |> roundup thy (add_reg thy export) export (name, morph)
    2.41 +      |> snd
    2.42        (* add mixin *)
    2.43        |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
    2.44        (* activate import hierarchy as far as not already active *)