eliminated odd object-oriented type_context/term_context;
export ProofContext.intern_skolem;
--- 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 *)
--- 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;