# HG changeset patch # User wenzelm # Date 1349102242 -7200 # Node ID dbadb4d03cbc79000ab7f3c3dca4ade9248811cd # Parent 2a088cff1e7b60c072fa1a589df855c5882493c1 report sort assignment of visible type variables; diff -r 2a088cff1e7b -r dbadb4d03cbc src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- 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 diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/Isar/proof_context.ML --- 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 *) diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/PIDE/isabelle_markup.ML --- 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"; diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/PIDE/isabelle_markup.scala --- 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" diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/Syntax/syntax.ML --- 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"]; diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/Syntax/syntax_phases.ML --- 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; diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/Syntax/term_position.ML --- 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 diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/pure_thy.ML --- 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 ("\\_", [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 "_"), diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/term.ML --- 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; diff -r 2a088cff1e7b -r dbadb4d03cbc src/Pure/variable.ML --- 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 diff -r 2a088cff1e7b -r dbadb4d03cbc src/Tools/jEdit/src/isabelle_rendering.scala --- 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)))