internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
authorwenzelm
Fri Oct 19 20:57:16 2007 +0200 (2007-10-19)
changeset 25105c9f67836c4d8
parent 25104 26b9a7db3386
child 25106 ff8fee9e752c
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Oct 19 20:57:14 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Oct 19 20:57:16 2007 +0200
     1.3 @@ -77,6 +77,9 @@
     1.4     else ProofContext.naming_of (LocalTheory.target_of lthy))
     1.5    |> NameSpace.qualified_names;
     1.6  
     1.7 +fun class_target (Target {target, ...}) f =
     1.8 +  LocalTheory.raw_theory f #>
     1.9 +  LocalTheory.target (Class.refresh_syntax target);
    1.10  
    1.11  
    1.12  (* notes *)
    1.13 @@ -159,11 +162,12 @@
    1.14    end;
    1.15  
    1.16  
    1.17 -(* consts *)
    1.18 +(* declare_const *)
    1.19  
    1.20 -fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
    1.21 -  | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
    1.22 -  | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
    1.23 +fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
    1.24 +  if not is_locale then (NoSyn, NoSyn, mx)
    1.25 +  else if not is_class then (NoSyn, mx, NoSyn)
    1.26 +  else (mx, NoSyn, NoSyn);
    1.27  
    1.28  fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
    1.29    let
    1.30 @@ -181,86 +185,57 @@
    1.31             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))
    1.32    end;
    1.33  
    1.34 -fun declare_consts (ta as Target {target, is_locale, is_class}) depends decls lthy =
    1.35 +fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy =
    1.36    let
    1.37      val pos = ContextPosition.properties_of lthy;
    1.38 -    val thy = ProofContext.theory_of lthy;
    1.39      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.40 -
    1.41 -    fun const ((c, T), mx) thy =
    1.42 -      let
    1.43 -        val U = map #2 xs ---> T;
    1.44 -        val (mx12, mx3) = fork_mixfix is_locale is_class mx;
    1.45 -        val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
    1.46 -        val t = Term.list_comb (const, map Free xs);
    1.47 -      in (((c, mx12), t), thy') end;
    1.48 -    fun class_const ((c, _), _) ((_, (mx1, _)), t) =
    1.49 -      LocalTheory.raw_theory_result (Class.add_logical_const target pos ((c, mx1), t))
    1.50 -      #> snd
    1.51 -      #> LocalTheory.target (Class.refresh_syntax target);
    1.52 -
    1.53 -    val (abbrs, lthy') = lthy
    1.54 -      |> LocalTheory.theory_result (fold_map const decls)
    1.55 -    val abbrs' = (map o apfst o apsnd) snd abbrs;
    1.56 +    val U = map #2 xs ---> T;
    1.57 +    val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.58 +    val (const, lthy') = lthy |> LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    1.59 +    val t = Term.list_comb (const, map Free xs);
    1.60    in
    1.61      lthy'
    1.62 -    |> is_locale ? fold (term_syntax ta o locale_const Syntax.mode_default pos) abbrs'
    1.63 -    |> is_class ? fold2 class_const decls abbrs
    1.64 -    |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs'
    1.65 +    |> is_locale ? term_syntax ta (locale_const Syntax.mode_default pos ((c, mx2), t))
    1.66 +    |> is_class ? class_target ta (Class.add_logical_const target pos ((c, mx1), t))
    1.67 +    |> LocalDefs.add_def ((c, NoSyn), t)
    1.68    end;
    1.69  
    1.70  
    1.71  (* abbrev *)
    1.72  
    1.73 -local
    1.74 -
    1.75 -fun context_abbrev pos (c, t) lthy = lthy
    1.76 -  |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
    1.77 -  |> LocalDefs.add_def ((c, NoSyn), t);
    1.78 -
    1.79 -fun class_abbrev target prmode pos ((c, mx), rhs) lthy = lthy
    1.80 -  |> LocalTheory.raw_theory_result
    1.81 -       (Class.add_syntactic_const target prmode pos ((c, mx), rhs))
    1.82 -  |> snd
    1.83 -  |> LocalTheory.target (Class.refresh_syntax target);
    1.84 -
    1.85 -in
    1.86 -
    1.87 -fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((raw_c, mx), raw_t) lthy =
    1.88 +fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((c, mx), t) lthy =
    1.89    let
    1.90      val pos = ContextPosition.properties_of lthy;
    1.91      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.92      val target_ctxt = LocalTheory.target_of lthy;
    1.93 -    val target_morphism = LocalTheory.target_morphism lthy;
    1.94 -    val c = Morphism.name target_morphism raw_c;
    1.95 -    val t = Morphism.term target_morphism raw_t;
    1.96 +
    1.97 +    val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.98 +    val t' = Assumption.export_term lthy target_ctxt t;
    1.99 +    val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
   1.100 +    val u = fold_rev lambda xs t';
   1.101 +    val global_rhs =
   1.102 +      singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
   1.103  
   1.104 -    val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
   1.105 -    val ((mx1, mx2), mx3) = fork_mixfix is_locale is_class mx;
   1.106 -
   1.107 -    val global_rhs =
   1.108 -      singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)
   1.109 -        (fold_rev lambda xs t);
   1.110 +    val lthy' =
   1.111 +      if is_locale then
   1.112 +        lthy
   1.113 +        |> LocalTheory.theory_result (Sign.add_abbrev Syntax.internalM pos (c, global_rhs))
   1.114 +        |-> (fn (lhs, _) =>
   1.115 +          let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
   1.116 +            term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
   1.117 +            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), lhs'))
   1.118 +          end)
   1.119 +      else
   1.120 +        lthy
   1.121 +        |> LocalTheory.theory
   1.122 +          (Sign.add_abbrev (#1 prmode) pos (c, global_rhs) #-> (fn (lhs, _) =>
   1.123 +           Sign.notation true prmode [(lhs, mx3)]))
   1.124    in
   1.125 -    if is_locale then
   1.126 -      lthy
   1.127 -      |> LocalTheory.theory_result (Sign.add_abbrev Syntax.internalM pos (c, global_rhs))
   1.128 -      |-> (fn (lhs, _) =>
   1.129 -        let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
   1.130 -          term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
   1.131 -          is_class ? class_abbrev target prmode pos ((c, mx1), lhs')
   1.132 -        end)
   1.133 -      |> context_abbrev pos (c, raw_t)
   1.134 -    else
   1.135 -      lthy
   1.136 -      |> LocalTheory.theory
   1.137 -        (Sign.add_abbrev (#1 prmode) pos (c, global_rhs)
   1.138 -          #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx3)]))
   1.139 -      |> context_abbrev pos (c, raw_t)
   1.140 +    lthy'
   1.141 +    |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
   1.142 +    |> LocalDefs.add_def ((c, NoSyn), t)
   1.143    end;
   1.144  
   1.145 -end;
   1.146 -
   1.147  
   1.148  (* define *)
   1.149  
   1.150 @@ -276,9 +251,8 @@
   1.151      val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
   1.152      val T = Term.fastype_of rhs;
   1.153  
   1.154 -    (*consts*)
   1.155 -    val ([(lhs, local_def)], lthy2) = lthy
   1.156 -      |> declare_consts ta (member (op =) xs) [((c, T), mx)];
   1.157 +    (*const*)
   1.158 +    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((c, T), mx);
   1.159      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
   1.160  
   1.161      (*def*)
   1.162 @@ -289,7 +263,7 @@
   1.163         (*global.c xs == rhs'*)  global_def,
   1.164         (*rhs' == rhs*)          Thm.symmetric rhs_conv];
   1.165  
   1.166 -    (*notes*)
   1.167 +    (*note*)
   1.168      val ([(res_name, [res])], lthy4) = lthy3
   1.169        |> notes ta kind [((name', atts), [([def], [])])];
   1.170    in ((lhs, (res_name, res)), lthy4) end;
   1.171 @@ -304,7 +278,7 @@
   1.172      val xs = fold Term.add_frees expanded_props [];
   1.173  
   1.174      (*consts*)
   1.175 -    val (consts, lthy') = declare_consts ta (member (op =) xs) vars lthy;
   1.176 +    val (consts, lthy') = fold_map (declare_const ta (member (op =) xs)) vars lthy;
   1.177      val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
   1.178  
   1.179      (*axioms*)