notation/abbreviation: more serious handling of morphisms;
authorwenzelm
Tue Dec 05 22:14:49 2006 +0100 (2006-12-05 ago)
changeset 21664dd4e89123359
parent 21663 734a9c3f562d
child 21665 ba07e24dc941
notation/abbreviation: more serious handling of morphisms;
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Tue Dec 05 22:14:48 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Dec 05 22:14:49 2006 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  fun target f = #2 o target_result (f #> pair ());
     1.5  
     1.6  
     1.7 -(* primitive operations *)
     1.8 +(* basic operations *)
     1.9  
    1.10  fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    1.11  fun operation1 f x = operation (fn ops => f ops x);
    1.12 @@ -163,22 +163,29 @@
    1.13  val target_morphism = operation #target_morphism;
    1.14  val target_name = operation #target_name;
    1.15  
    1.16 -
    1.17 -(* derived operations *)
    1.18 -
    1.19  fun def kind arg lthy = lthy |> defs kind [arg] |>> hd;
    1.20 -
    1.21  fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
    1.22  
    1.23 -fun notation mode args = term_syntax (fn phi =>
    1.24 -  let val args' = args |> map (fn (t, mx) => (Morphism.term phi t, mx))
    1.25 -  in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end);
    1.26 +
    1.27 +(* term syntax *)
    1.28 +
    1.29 +fun generic_notation mode args phi =
    1.30 +  let
    1.31 +    val args' = args |> filter (fn (t, _) => t aconv Morphism.term phi t);
    1.32 +  in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end;
    1.33 +
    1.34 +fun notation mode args = term_syntax (generic_notation mode args);
    1.35  
    1.36  fun abbrevs mode args = term_syntax (fn phi =>
    1.37 -  let val args' = args |> map (fn ((c, mx), t) => ((Morphism.name phi c, mx), Morphism.term phi t))
    1.38 +  let
    1.39 +    val (mxs, args') = args |> map_filter (fn ((c, mx), t) =>
    1.40 +        if t aconv Morphism.term phi t
    1.41 +        then SOME (mx, ((Morphism.name phi c, NoSyn), t))
    1.42 +        else NONE)
    1.43 +      |> split_list;
    1.44    in
    1.45 -    Context.mapping
    1.46 -      (snd o Sign.add_abbrevs mode args') (snd o ProofContext.add_abbrevs mode args')
    1.47 +    Context.mapping_result (Sign.add_abbrevs mode args') (ProofContext.add_abbrevs mode args')
    1.48 +    #-> (fn abbrs => generic_notation mode (map #1 abbrs ~~ mxs) phi)
    1.49    end);
    1.50  
    1.51