# HG changeset patch # User wenzelm # Date 1394101936 -3600 # Node ID 3bb5c717923492f8ffab97048930065d8f3bbf36 # Parent 4766342e8376ce9660b0bbdf671b0e55924dd166 clarified treatment of consts -- prefer value-oriented reports; diff -r 4766342e8376 -r 3bb5c7179234 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 06 10:53:14 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 11:32:16 2014 +0100 @@ -74,6 +74,8 @@ xstring * Position.T -> typ * Position.report list val read_type_name: Proof.context -> bool -> string -> typ val read_type_name_proper: Proof.context -> bool -> string -> typ + val check_const_proper: Proof.context -> bool -> + xstring * Position.T -> term * Position.report list val read_const_proper: Proof.context -> bool -> string -> term val read_const: Proof.context -> bool -> typ -> string -> term val read_arity: Proof.context -> xstring * string list * string -> arity @@ -82,7 +84,6 @@ 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 val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term @@ -474,45 +475,49 @@ (* constant names *) -local - -fun prep_const_proper ctxt strict (c, pos) = +fun check_const_proper ctxt strict (c, pos) = let fun err msg = error (msg ^ Position.here pos); val consts = consts_of ctxt; - val t as Const (d, _) = + val (t as Const (d, _), reports) = (case Variable.lookup_const ctxt c of SOME d => let val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg; - val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d); - in Const (d, T) end + val reports = + if Context_Position.is_reported ctxt pos + then [(pos, Name_Space.markup (Consts.space_of consts) d)] else []; + in (Const (d, T), reports) end | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos)); val _ = if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg else (); - in t end; + in (t, reports) end; -in - -fun read_const_proper ctxt strict = - prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token; +fun read_const_proper ctxt strict text = + let + val (t, reports) = + check_const_proper ctxt strict (Symbol_Pos.source_content (Syntax.read_token text)); + val _ = Position.reports reports; + in t end; fun read_const ctxt strict ty text = let val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text); val _ = Name.reject_internal (c, [pos]); - in - (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of - (SOME x, false) => - (Context_Position.report ctxt pos - (Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)); - Free (x, infer_type ctxt (x, ty))) - | _ => prep_const_proper ctxt strict (c, pos)) - end; - -end; + val (t, reports) = + (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of + (SOME x, false) => + let + val reports = + if Context_Position.is_reported ctxt pos + then [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))] + else []; + in (Free (x, infer_type ctxt (x, ty)), reports) end + | _ => check_const_proper ctxt strict (c, pos)); + val _ = Position.reports reports; + in t end; (* type arities *) @@ -533,21 +538,6 @@ end; -(* skolem variables *) - -fun intern_skolem ctxt x = - let - val skolem = Variable.lookup_fixed ctxt x; - val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x; - val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); - in - if Variable.is_const ctxt x then NONE - else if is_some skolem then skolem - else if not is_const orelse is_declared then SOME x - else NONE - end; - - (* read_term *) fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); diff -r 4766342e8376 -r 3bb5c7179234 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 10:53:14 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 11:32:16 2014 +0100 @@ -220,13 +220,27 @@ (* decode_term -- transform parse tree into raw term *) +fun decode_const ctxt c = + let val (Const (c', _), _) = Proof_Context.check_const_proper ctxt false (c, Position.none) + in c' end; + fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result | decode_term ctxt (reports0, Exn.Res tm) = let - fun get_const a = - ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a))) - handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a)); - val get_free = Proof_Context.intern_skolem ctxt; + fun get_const c = + (true, decode_const ctxt c) handle ERROR _ => + (false, Consts.intern (Proof_Context.consts_of ctxt) c); + fun get_free x = + let + val skolem = Variable.lookup_fixed ctxt x; + val is_const = can (decode_const ctxt) x orelse Long_Name.is_qualified x; + val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); + in + if Variable.is_const ctxt x then NONE + else if is_some skolem then skolem + else if not is_const orelse is_declared then SOME x + else NONE + end; val reports = Unsynchronized.ref reports0; fun report ps = Position.store_reports reports ps; @@ -796,7 +810,7 @@ fun const_ast_tr intern ctxt [Ast.Variable c] = let - val Const (c', _) = Proof_Context.read_const_proper ctxt false c; + val c' = decode_const ctxt c; val d = if intern then Lexicon.mark_const c' else c; in Ast.Constant d end | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] = diff -r 4766342e8376 -r 3bb5c7179234 src/Pure/consts.ML --- a/src/Pure/consts.ML Thu Mar 06 10:53:14 2014 +0100 +++ b/src/Pure/consts.ML Thu Mar 06 11:32:16 2014 +0100 @@ -25,7 +25,7 @@ val extern: Proof.context -> T -> string -> xstring val intern_syntax: T -> xstring -> string val extern_syntax: Proof.context -> T -> string -> xstring - val check_const: Context.generic -> T -> xstring * Position.T -> term + val check_const: Context.generic -> T -> xstring * Position.T -> term * Position.report list val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list val instance: T -> string * typ list -> typ @@ -146,9 +146,9 @@ fun check_const context consts (xname, pos) = let val Consts {decls, ...} = consts; - val (c, _) = Name_Space.check context decls (xname, pos); + val ((c, reports), _) = Name_Space.check_reports context decls (xname, pos); val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos); - in Const (c, T) end; + in (Const (c, T), reports) end; (* certify *)