better drop background syntax if entity depends on parameters;
authorwenzelm
Tue Apr 03 16:10:34 2012 +0200 (2012-04-03)
changeset 472916a641856a0e9
parent 47290 ba9c8613ad9b
child 47292 1884d34e9aab
better drop background syntax if entity depends on parameters;
more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
src/Pure/Isar/generic_target.ML
src/Pure/type_infer_context.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 14:37:16 2012 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 16:10:34 2012 +0200
     1.3 @@ -60,6 +60,11 @@
     1.4           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
     1.5        NoSyn);
     1.6  
     1.7 +fun check_mixfix_global (b, no_params) mx =
     1.8 +  if no_params orelse mx = NoSyn then mx
     1.9 +  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
    1.10 +    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
    1.11 +
    1.12  
    1.13  (* define *)
    1.14  
    1.15 @@ -236,13 +241,10 @@
    1.16              let
    1.17                val thy = Context.theory_of context;
    1.18                val ctxt = Context.proof_of context;
    1.19 -              val t' = Syntax.check_term ctxt (Const (c, dummyT))
    1.20 -                |> singleton (Variable.polymorphic ctxt);
    1.21              in
    1.22 -              (case t' of
    1.23 -                Const (c', T') =>
    1.24 -                  if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
    1.25 -              | _ => NONE)
    1.26 +              (case Type_Infer_Context.const_type ctxt c of
    1.27 +                SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
    1.28 +              | NONE => NONE)
    1.29              end
    1.30          | _ => NONE)
    1.31        else NONE;
    1.32 @@ -274,9 +276,13 @@
    1.33  
    1.34  fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    1.35    let
    1.36 +    val params = type_params @ term_params;
    1.37 +    val mx' = check_mixfix_global (b, null params) mx;
    1.38 +
    1.39      val (const, lthy2) = lthy
    1.40 -      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
    1.41 -    val lhs = list_comb (const, type_params @ term_params);
    1.42 +      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
    1.43 +    val lhs = Term.list_comb (const, params);
    1.44 +
    1.45      val ((_, def), lthy3) = lthy2
    1.46        |> Local_Theory.background_theory_result
    1.47          (Thm.add_def lthy2 false false
    1.48 @@ -301,7 +307,8 @@
    1.49  fun theory_abbrev prmode (b, mx) (t, _) xs =
    1.50    Local_Theory.background_theory_result
    1.51      (Sign.add_abbrev (#1 prmode) (b, t) #->
    1.52 -      (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)] #> pair lhs))
    1.53 +      (fn (lhs, _) =>  (* FIXME type_params!? *)
    1.54 +        Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
    1.55    #-> (fn lhs => fn lthy' => lthy' |>
    1.56          const_declaration (fn level => level <> Local_Theory.level lthy') prmode
    1.57            ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
     2.1 --- a/src/Pure/type_infer_context.ML	Tue Apr 03 14:37:16 2012 +0200
     2.2 +++ b/src/Pure/type_infer_context.ML	Tue Apr 03 16:10:34 2012 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  signature TYPE_INFER_CONTEXT =
     2.5  sig
     2.6    val const_sorts: bool Config.T
     2.7 +  val const_type: Proof.context -> string -> typ option
     2.8    val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
     2.9    val prepare: Proof.context -> term list -> int * term list
    2.10    val infer_types: Proof.context -> term list -> term list