src/Pure/Isar/theory_target.ML
changeset 35764 f7f88f2e004f
parent 35739 35a3b3721ffb
child 35765 09e238561460
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Mar 13 17:19:12 2010 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Mar 13 19:35:53 2010 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(* declare_const *)
     1.8 +(* consts *)
     1.9  
    1.10  fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
    1.11    if not is_locale then (NoSyn, NoSyn, mx)
    1.12 @@ -209,34 +209,6 @@
    1.13               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    1.14    end;
    1.15  
    1.16 -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    1.17 -
    1.18 -fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    1.19 -  let
    1.20 -    val xs = filter depends (#1 (ProofContext.inferred_fixes (Local_Theory.target_of lthy)));
    1.21 -    val U = map #2 xs ---> T;
    1.22 -    val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.23 -    val (const, lthy') = lthy |>
    1.24 -      (case Class_Target.instantiation_param lthy b of
    1.25 -        SOME c' =>
    1.26 -          if mx3 <> NoSyn then syntax_error c'
    1.27 -          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
    1.28 -            ##> Class_Target.confirm_declaration b
    1.29 -        | NONE =>
    1.30 -            (case Overloading.operation lthy b of
    1.31 -              SOME (c', _) =>
    1.32 -                if mx3 <> NoSyn then syntax_error c'
    1.33 -                else Local_Theory.theory_result (Overloading.declare (c', U))
    1.34 -                  ##> Overloading.confirm b
    1.35 -            | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
    1.36 -    val t = Term.list_comb (const, map Free xs);
    1.37 -  in
    1.38 -    lthy'
    1.39 -    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
    1.40 -    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
    1.41 -    |> Local_Defs.add_def ((b, NoSyn), t)
    1.42 -  end;
    1.43 -
    1.44  
    1.45  (* abbrev *)
    1.46  
    1.47 @@ -271,6 +243,43 @@
    1.48  
    1.49  (* define *)
    1.50  
    1.51 +local
    1.52 +
    1.53 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    1.54 +
    1.55 +fun declare_const (ta as Target {target, is_locale, is_class, ...}) xs ((b, T), mx) lthy =
    1.56 +  let
    1.57 +    val params =
    1.58 +      rev (Variable.fixes_of (Local_Theory.target_of lthy))
    1.59 +      |> map_filter (fn (_, x) =>
    1.60 +        (case AList.lookup (op =) xs x of
    1.61 +          SOME T => SOME (x, T)
    1.62 +        | NONE => NONE));
    1.63 +    val U = map #2 params ---> T;
    1.64 +    val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.65 +    val (const, lthy') = lthy |>
    1.66 +      (case Class_Target.instantiation_param lthy b of
    1.67 +        SOME c' =>
    1.68 +          if mx3 <> NoSyn then syntax_error c'
    1.69 +          else Local_Theory.theory_result (AxClass.declare_overloaded (c', U))
    1.70 +            ##> Class_Target.confirm_declaration b
    1.71 +      | NONE =>
    1.72 +          (case Overloading.operation lthy b of
    1.73 +            SOME (c', _) =>
    1.74 +              if mx3 <> NoSyn then syntax_error c'
    1.75 +              else Local_Theory.theory_result (Overloading.declare (c', U))
    1.76 +                ##> Overloading.confirm b
    1.77 +          | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
    1.78 +    val t = Term.list_comb (const, map Free params);
    1.79 +  in
    1.80 +    lthy'
    1.81 +    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
    1.82 +    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
    1.83 +    |> Local_Defs.add_def ((b, NoSyn), t)
    1.84 +  end;
    1.85 +
    1.86 +in
    1.87 +
    1.88  fun define ta ((b, mx), ((name, atts), rhs)) lthy =
    1.89    let
    1.90      val thy = ProofContext.theory_of lthy;
    1.91 @@ -286,7 +295,7 @@
    1.92      val T = Term.fastype_of rhs;
    1.93  
    1.94      (*const*)
    1.95 -    val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx);
    1.96 +    val ((lhs, local_def), lthy2) = lthy |> declare_const ta xs ((b, T), mx);
    1.97      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.98  
    1.99      (*def*)
   1.100 @@ -295,9 +304,9 @@
   1.101          (case Overloading.operation lthy b of
   1.102            SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs')
   1.103          | NONE =>
   1.104 -            if is_none (Class_Target.instantiation_param lthy b)
   1.105 -            then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
   1.106 -            else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
   1.107 +            if is_some (Class_Target.instantiation_param lthy b)
   1.108 +            then AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs')
   1.109 +            else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')));
   1.110      val def = Local_Defs.trans_terms lthy3
   1.111        [(*c == global.c xs*)     local_def,
   1.112         (*global.c xs == rhs'*)  global_def,
   1.113 @@ -308,6 +317,8 @@
   1.114        |> notes ta "" [((name', atts), [([def], [])])];
   1.115    in ((lhs, (res_name, res)), lthy4) end;
   1.116  
   1.117 +end;
   1.118 +
   1.119  
   1.120  (* init various targets *)
   1.121