src/Pure/Isar/proof_context.ML
changeset 49674 dbadb4d03cbc
parent 48992 0518bf89c777
child 49685 4341e4d86872
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Oct 01 12:05:05 2012 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Oct 01 16:37:22 2012 +0200
     1.3 @@ -70,7 +70,8 @@
     1.4    val read_arity: Proof.context -> xstring * string list * string -> arity
     1.5    val cert_arity: Proof.context -> arity -> arity
     1.6    val allow_dummies: Proof.context -> Proof.context
     1.7 -  val prepare_sorts: Proof.context -> typ list -> typ list
     1.8 +  val prepare_sortsT: Proof.context -> typ list -> string * typ list
     1.9 +  val prepare_sorts: Proof.context -> term list -> string * term list
    1.10    val check_tfree: Proof.context -> string * sort -> string * sort
    1.11    val intern_skolem: Proof.context -> string -> string option
    1.12    val read_term_pattern: Proof.context -> string -> term
    1.13 @@ -615,13 +616,15 @@
    1.14  
    1.15  (* sort constraints *)
    1.16  
    1.17 -fun prepare_sorts ctxt tys =
    1.18 +local
    1.19 +
    1.20 +fun prepare_sorts_env ctxt tys =
    1.21    let
    1.22      val tsig = tsig_of ctxt;
    1.23      val defaultS = Type.defaultS tsig;
    1.24  
    1.25      fun constraint (xi, S) env =
    1.26 -      if S = dummyS then env
    1.27 +      if S = dummyS orelse Term_Position.is_positionS S then env
    1.28        else
    1.29          Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
    1.30            handle Vartab.DUP _ =>
    1.31 @@ -644,18 +647,57 @@
    1.32              error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
    1.33                " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
    1.34                " for type variable " ^ quote (Term.string_of_vname' xi)));
    1.35 -  in
    1.36 -    (map o map_atyps)
    1.37 -      (fn T =>
    1.38 -        if Term_Position.is_positionT T then T
    1.39 -        else
    1.40 -          (case T of
    1.41 -            TFree (x, _) => TFree (x, get_sort (x, ~1))
    1.42 -          | TVar (xi, _) => TVar (xi, get_sort xi)
    1.43 -          | _ => T)) tys
    1.44 -  end;
    1.45 +
    1.46 +    fun add_report raw_S S reports =
    1.47 +      (case Term_Position.decode_positionS raw_S of
    1.48 +        SOME pos =>
    1.49 +          if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
    1.50 +            (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
    1.51 +              :: reports
    1.52 +          else reports
    1.53 +      | NONE => reports);
    1.54 +
    1.55 +    val reports =
    1.56 +      (fold o fold_atyps)
    1.57 +        (fn T =>
    1.58 +          if Term_Position.is_positionT T then I
    1.59 +          else
    1.60 +            (case T of
    1.61 +              TFree (x, raw_S) => add_report raw_S (get_sort (x, ~1))
    1.62 +            | TVar (xi, raw_S) => add_report raw_S (get_sort xi)
    1.63 +            | _ => I)) tys [];
    1.64 +
    1.65 +  in (implode (map #2 reports), get_sort) end;
    1.66  
    1.67 -fun check_tfree ctxt v = dest_TFree (singleton (prepare_sorts ctxt) (TFree v));
    1.68 +fun replace_sortsT get_sort =
    1.69 +  map_atyps
    1.70 +    (fn T =>
    1.71 +      if Term_Position.is_positionT T then T
    1.72 +      else
    1.73 +        (case T of
    1.74 +          TFree (x, _) => TFree (x, get_sort (x, ~1))
    1.75 +        | TVar (xi, _) => TVar (xi, get_sort xi)
    1.76 +        | _ => T));
    1.77 +
    1.78 +in
    1.79 +
    1.80 +fun prepare_sortsT ctxt tys =
    1.81 +  let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys
    1.82 +  in (sorting_report, map (replace_sortsT get_sort) tys) end;
    1.83 +
    1.84 +fun prepare_sorts ctxt tms =
    1.85 +  let
    1.86 +    val tys = rev ((fold o fold_types) cons tms []);
    1.87 +    val (sorting_report, get_sort) = prepare_sorts_env ctxt tys;
    1.88 +  in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end;
    1.89 +
    1.90 +fun check_tfree ctxt v =
    1.91 +  let
    1.92 +    val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
    1.93 +    val _ = Context_Position.if_visible ctxt Output.report sorting_report;
    1.94 +  in a end;
    1.95 +
    1.96 +end;
    1.97  
    1.98  
    1.99  (* certify terms *)