# HG changeset patch # User wenzelm # Date 1302095439 -7200 # Node ID cc5ac538f99180efd9f6f182c7773baf8d9588a5 # Parent 12a0736705847a61948e544c191351b983c6684a eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem; diff -r 12a073670584 -r cc5ac538f991 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Apr 06 14:44:40 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Apr 06 15:10:39 2011 +0200 @@ -64,14 +64,11 @@ val read_const_proper: Proof.context -> bool -> string -> term val read_const: Proof.context -> bool -> typ -> string -> term val allow_dummies: Proof.context -> Proof.context + val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort - val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort - type type_context - val type_context: Proof.context -> type_context - type term_context - val term_context: Proof.context -> term_context val standard_infer_types: Proof.context -> term list -> term list + 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 @@ -266,7 +263,6 @@ fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; val consts_of = #1 o #consts o rep_context; -val const_space = Consts.space_of o consts_of; val the_const_constraint = Consts.the_constraint o consts_of; val facts_of = #facts o rep_context; @@ -526,6 +522,22 @@ end; +(* skolem variables *) + +fun intern_skolem ctxt x = + let + val _ = no_skolem false x; + val sko = lookup_skolem 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 sko then sko + 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); @@ -618,9 +630,7 @@ end; -(* decoding raw terms (syntax trees) *) - -(* types *) +(* sort constraints *) fun get_sort ctxt raw_text = let @@ -653,54 +663,6 @@ fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi); fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S)); -local - -fun intern_skolem ctxt def_type x = - let - val _ = no_skolem false x; - val sko = lookup_skolem ctxt x; - val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x; - val is_declared = is_some (def_type (x, ~1)); - in - if Variable.is_const ctxt x then NONE - else if is_some sko then sko - else if not is_const orelse is_declared then SOME x - else NONE - end; - -in - -type type_context = - {get_class: string -> string, - get_type: string -> string, - markup_class: string -> Markup.T list, - markup_type: string -> Markup.T list}; - -fun type_context ctxt : type_context = - {get_class = read_class ctxt, - get_type = #1 o dest_Type o read_type_name_proper ctxt false, - markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c], - markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]}; - -type term_context = - {get_const: string -> bool * string, - get_free: string -> string option, - markup_const: string -> Markup.T list, - markup_free: string -> Markup.T list, - markup_var: indexname -> Markup.T list}; - -fun term_context ctxt : term_context = - {get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) - handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), - get_free = intern_skolem ctxt (Variable.def_type ctxt false), - markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c], - markup_free = fn x => - [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ - (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]), - markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]}; - -end; - (* certify terms *) diff -r 12a073670584 -r cc5ac538f991 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 14:44:40 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 15:10:39 2011 +0200 @@ -93,7 +93,12 @@ fun parsetree_to_ast ctxt constrain_pos trf parsetree = let - val {get_class, get_type, markup_class, markup_type} = ProofContext.type_context ctxt; + val tsig = ProofContext.tsig_of ctxt; + + val get_class = ProofContext.read_class ctxt; + val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false; + fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c]; + fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c]; val reports = Unsynchronized.ref ([]: Position.reports); fun report pos = Position.reports reports [pos]; @@ -146,14 +151,23 @@ (* decode_term -- transform parse tree into raw term *) -fun markup_bound def id = - [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound]; - fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result | decode_term ctxt (reports0, Exn.Result tm) = let - val {get_const, get_free, markup_const, markup_free, markup_var} = - ProofContext.term_context ctxt; + val consts = ProofContext.consts_of ctxt; + fun get_const a = + ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a))) + handle ERROR _ => (false, Consts.intern consts a)); + val get_free = ProofContext.intern_skolem ctxt; + fun markup_const c = [Name_Space.markup_entry (Consts.space_of consts) c]; + fun markup_free x = + [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ + (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] + else [Markup.hilite]); + fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; + fun markup_bound def id = + [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound]; + val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm)); val reports = Unsynchronized.ref reports0;