--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Oct 01 12:05:05 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Oct 01 16:37:22 2012 +0200
@@ -30,11 +30,13 @@
parse_translation {*
let
fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
- fun finite_vec_tr [t, u as Free (x, _)] =
+ fun finite_vec_tr [t, u] =
+ (case Term_Position.strip_positions u of
+ v as Free (x, _) =>
if Lexicon.is_tid x then
- vec t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
+ vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax finite})
else vec t u
- | finite_vec_tr [t, u] = vec t u
+ | _ => vec t u)
in
[(@{syntax_const "_finite_vec"}, finite_vec_tr)]
end
--- a/src/Pure/Isar/proof_context.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Oct 01 16:37:22 2012 +0200
@@ -70,7 +70,8 @@
val read_arity: Proof.context -> xstring * string list * string -> arity
val cert_arity: Proof.context -> arity -> arity
val allow_dummies: Proof.context -> Proof.context
- val prepare_sorts: Proof.context -> typ list -> typ list
+ val prepare_sortsT: Proof.context -> typ list -> string * typ list
+ val prepare_sorts: Proof.context -> term list -> string * term list
val check_tfree: Proof.context -> string * sort -> string * sort
val intern_skolem: Proof.context -> string -> string option
val read_term_pattern: Proof.context -> string -> term
@@ -615,13 +616,15 @@
(* sort constraints *)
-fun prepare_sorts ctxt tys =
+local
+
+fun prepare_sorts_env ctxt tys =
let
val tsig = tsig_of ctxt;
val defaultS = Type.defaultS tsig;
fun constraint (xi, S) env =
- if S = dummyS then env
+ if S = dummyS orelse Term_Position.is_positionS S then env
else
Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
handle Vartab.DUP _ =>
@@ -644,18 +647,57 @@
error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
" inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
" for type variable " ^ quote (Term.string_of_vname' xi)));
- in
- (map o map_atyps)
- (fn T =>
- if Term_Position.is_positionT T then T
- else
- (case T of
- TFree (x, _) => TFree (x, get_sort (x, ~1))
- | TVar (xi, _) => TVar (xi, get_sort xi)
- | _ => T)) tys
- end;
+
+ fun add_report raw_S S reports =
+ (case Term_Position.decode_positionS raw_S of
+ SOME pos =>
+ if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
+ (pos, Position.reported_text pos Isabelle_Markup.sorting (Syntax.string_of_sort ctxt S))
+ :: reports
+ else reports
+ | NONE => reports);
+
+ val reports =
+ (fold o fold_atyps)
+ (fn T =>
+ if Term_Position.is_positionT T then I
+ else
+ (case T of
+ TFree (x, raw_S) => add_report raw_S (get_sort (x, ~1))
+ | TVar (xi, raw_S) => add_report raw_S (get_sort xi)
+ | _ => I)) tys [];
+
+ in (implode (map #2 reports), get_sort) end;
-fun check_tfree ctxt v = dest_TFree (singleton (prepare_sorts ctxt) (TFree v));
+fun replace_sortsT get_sort =
+ map_atyps
+ (fn T =>
+ if Term_Position.is_positionT T then T
+ else
+ (case T of
+ TFree (x, _) => TFree (x, get_sort (x, ~1))
+ | TVar (xi, _) => TVar (xi, get_sort xi)
+ | _ => T));
+
+in
+
+fun prepare_sortsT ctxt tys =
+ let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys
+ in (sorting_report, map (replace_sortsT get_sort) tys) end;
+
+fun prepare_sorts ctxt tms =
+ let
+ val tys = rev ((fold o fold_types) cons tms []);
+ val (sorting_report, get_sort) = prepare_sorts_env ctxt tys;
+ in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end;
+
+fun check_tfree ctxt v =
+ let
+ val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
+ val _ = Context_Position.if_visible ctxt Output.report sorting_report;
+ in a end;
+
+end;
(* certify terms *)
--- a/src/Pure/PIDE/isabelle_markup.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Mon Oct 01 16:37:22 2012 +0200
@@ -48,6 +48,7 @@
val typN: string val typ: Markup.T
val termN: string val term: Markup.T
val propN: string val prop: Markup.T
+ val sortingN: string val sorting: Markup.T
val typingN: string val typing: Markup.T
val ML_keywordN: string val ML_keyword: Markup.T
val ML_delimiterN: string val ML_delimiter: Markup.T
@@ -200,6 +201,7 @@
val (termN, term) = markup_elem "term";
val (propN, prop) = markup_elem "prop";
+val (sortingN, sorting) = markup_elem "sorting";
val (typingN, typing) = markup_elem "typing";
--- a/src/Pure/PIDE/isabelle_markup.scala Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Mon Oct 01 16:37:22 2012 +0200
@@ -108,6 +108,7 @@
val TERM = "term"
val PROP = "prop"
+ val SORTING = "sorting"
val TYPING = "typing"
val ATTRIBUTE = "attribute"
--- a/src/Pure/Syntax/syntax.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Oct 01 16:37:22 2012 +0200
@@ -539,11 +539,12 @@
["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
val basic_nonterms =
- (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
+ Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
- "float_position", "xnum_position", "index", "struct", "id_position",
- "longid_position", "str_position", "type_name", "class_name"]);
+ "float_position", "xnum_position", "index", "struct", "tid_position",
+ "tvar_position", "id_position", "longid_position", "str_position",
+ "type_name", "class_name"];
--- a/src/Pure/Syntax/syntax_phases.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Oct 01 16:37:22 2012 +0200
@@ -86,14 +86,16 @@
fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+ fun class_pos s = if is_some (Term_Position.decode s) then s else err ();
fun classes (Const (s, _)) = [class s]
| classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
| classes _ = err ();
fun sort (Const ("_topsort", _)) = []
+ | sort (Const ("_sort", _) $ cs) = classes cs
| sort (Const (s, _)) = [class s]
- | sort (Const ("_sort", _) $ cs) = classes cs
+ | sort (Free (s, _)) = [class_pos s]
| sort _ = err ();
in sort tm end;
@@ -138,7 +140,18 @@
NONE => Ast.mk_appl (Ast.Constant a) args
| SOME f => f ctxt args);
- fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
+ fun asts_of_token tok =
+ if Lexicon.valued_token tok
+ then [Ast.Variable (Lexicon.str_of_token tok)]
+ else [];
+
+ fun asts_of_position c tok =
+ if raw then asts_of_token tok
+ else
+ [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok),
+ Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
+
+ and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
let
val pos = Lexicon.pos_of_token tok;
val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
@@ -153,11 +166,8 @@
handle ERROR msg => error (msg ^ Position.here pos);
val _ = report pos (markup_type ctxt) c;
in [Ast.Constant (Lexicon.mark_type c)] end
- | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
- if raw then [ast_of pt]
- else
- [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
- Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
+ | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
+ | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
| asts_of (Parser.Node (a, pts)) =
let
val _ = pts |> List.app
@@ -165,10 +175,7 @@
if Lexicon.valued_token tok then ()
else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
in [trans a (maps asts_of pts)] end
- | asts_of (Parser.Tip tok) =
- if Lexicon.valued_token tok
- then [Ast.Variable (Lexicon.str_of_token tok)]
- else []
+ | asts_of (Parser.Tip tok) = asts_of_token tok
and ast_of pt =
(case asts_of pt of
@@ -823,27 +830,34 @@
in
-fun check_typs ctxt =
- Proof_Context.prepare_sorts ctxt #>
- apply_typ_check ctxt #>
- Term_Sharing.typs (Proof_Context.theory_of ctxt);
+fun check_typs ctxt raw_tys =
+ let
+ val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
+ val _ = Context_Position.if_visible ctxt Output.report sorting_report;
+ in
+ tys
+ |> apply_typ_check ctxt
+ |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
+ end;
fun check_terms ctxt raw_ts =
let
- val (ts, ps) = raw_ts
- |> Term.burrow_types (Proof_Context.prepare_sorts ctxt)
- |> Type_Infer_Context.prepare_positions ctxt;
+ val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
+ val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
+
val tys = map (Logic.mk_type o snd) ps;
val (ts', tys') = ts @ tys
|> apply_term_check ctxt
|> chop (length ts);
- val _ =
- map2 (fn (pos, _) => fn ty =>
+ val typing_report =
+ fold2 (fn (pos, _) => fn ty =>
if Position.is_reported pos then
- Markup.markup (Position.markup pos Isabelle_Markup.typing)
- (Syntax.string_of_typ ctxt (Logic.dest_type ty))
- else "") ps tys'
- |> implode |> Output.report
+ cons (Position.reported_text pos Isabelle_Markup.typing
+ (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
+ else I) ps tys' []
+ |> implode;
+
+ val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
--- a/src/Pure/Syntax/term_position.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/Syntax/term_position.ML Mon Oct 01 16:37:22 2012 +0200
@@ -11,8 +11,10 @@
val decode: string -> Position.T option
val decode_position: term -> (Position.T * typ) option
val decode_positionT: typ -> Position.T option
+ val decode_positionS: sort -> Position.T option
val is_position: term -> bool
val is_positionT: typ -> bool
+ val is_positionS: sort -> bool
val strip_positions: term -> term
end;
@@ -50,11 +52,15 @@
fun decode_positionT (TFree (x, _)) = decode x
| decode_positionT _ = NONE;
+fun decode_positionS [x] = decode x
+ | decode_positionS _ = NONE;
+
val is_position = is_some o decode_position;
val is_positionT = is_some o decode_positionT;
+val is_positionS = is_some o decode_positionS;
fun strip_positions ((t as Const (c, _)) $ u $ v) =
- if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
+ if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
then strip_positions u
else t $ strip_positions u $ strip_positions v
| strip_positions (t $ u) = strip_positions t $ strip_positions u
--- a/src/Pure/pure_thy.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/pure_thy.ML Mon Oct 01 16:37:22 2012 +0200
@@ -70,8 +70,8 @@
("", typ "prop' => prop'", Delimfix "'(_')"),
("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)),
- ("", typ "tid => type", Delimfix "_"),
- ("", typ "tvar => type", Delimfix "_"),
+ ("", typ "tid_position => type", Delimfix "_"),
+ ("", typ "tvar_position => type", Delimfix "_"),
("", typ "type_name => type", Delimfix "_"),
("_type_name", typ "id => type_name", Delimfix "_"),
("_type_name", typ "longid => type_name", Delimfix "_"),
@@ -137,6 +137,8 @@
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("_update_name", typ "idt", NoSyn),
("_constrainAbs", typ "'a", NoSyn),
+ ("_position_sort", typ "tid => tid_position", Delimfix "_"),
+ ("_position_sort", typ "tvar => tvar_position", Delimfix "_"),
("_position", typ "id => id_position", Delimfix "_"),
("_position", typ "longid => longid_position", Delimfix "_"),
("_position", typ "str_token => str_position", Delimfix "_"),
--- a/src/Pure/term.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/term.ML Mon Oct 01 16:37:22 2012 +0200
@@ -467,7 +467,7 @@
fun burrow_types f ts =
let
- val Ts = rev (fold (fold_types cons) ts []);
+ val Ts = rev ((fold o fold_types) cons ts []);
val Ts' = f Ts;
val (ts', []) = fold_map replace_types ts Ts';
in ts' end;
--- a/src/Pure/variable.ML Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/variable.ML Mon Oct 01 16:37:22 2012 +0200
@@ -214,7 +214,8 @@
(* constraints *)
fun constrain_tvar (xi, S) =
- if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);
+ if S = dummyS orelse Term_Position.is_positionS S
+ then Vartab.delete_safe xi else Vartab.update (xi, S);
fun declare_constraints t = map_constraints (fn (types, sorts) =>
let
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Oct 01 16:37:22 2012 +0200
@@ -181,9 +181,9 @@
private val highlight_include =
Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
- Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
- Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
- Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
+ Isabelle_Markup.PATH, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.FREE,
+ Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE,
+ Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
@@ -299,8 +299,8 @@
Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
private val tooltip_elements =
- Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
- Isabelle_Markup.PATH) ++ tooltips.keys
+ Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
+ Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
private def string_of_typing(kind: String, body: XML.Body): String =
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
@@ -322,7 +322,8 @@
if Path.is_ok(name) =>
val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
add(prev, r, (true, "file " + quote(jedit_file)))
- case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
+ case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
+ if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
add(prev, r, (true, string_of_typing("::", body)))
case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
add(prev, r, (false, string_of_typing("ML:", body)))