# HG changeset patch # User wenzelm # Date 1271347221 -7200 # Node ID 34d1ce2d746d356be3fb871b4626e19a66a85eac # Parent b89a2a05a3cedc6045f437c4828942e4e99bfb68 get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned; diff -r b89a2a05a3ce -r 34d1ce2d746d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 15 16:58:12 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 15 18:00:21 2010 +0200 @@ -62,6 +62,8 @@ val read_const_proper: Proof.context -> bool -> string -> term val read_const: Proof.context -> bool -> string -> term val allow_dummies: Proof.context -> Proof.context + val check_tvar: Proof.context -> indexname * sort -> indexname * sort + val check_tfree: Proof.context -> string * sort -> string * sort val decode_term: Proof.context -> term -> term val standard_infer_types: Proof.context -> term list -> term list val read_term_pattern: Proof.context -> string -> term @@ -606,19 +608,26 @@ (* types *) -fun get_sort ctxt def_sort raw_env = +fun get_sort ctxt raw_env = let val tsig = tsig_of ctxt; fun eq ((xi, S), (xi', S')) = Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S'); val env = distinct eq raw_env; - val _ = (case duplicates (eq_fst (op =)) env of [] => () + val _ = + (case duplicates (eq_fst (op =)) env of + [] => () | dups => error ("Inconsistent sort constraints for type variable(s) " ^ commas_quote (map (Term.string_of_vname' o fst) dups))); + fun lookup xi = + (case AList.lookup (op =) env xi of + NONE => NONE + | SOME S => if S = dummyS then NONE else SOME S); + fun get xi = - (case (AList.lookup (op =) env xi, def_sort xi) of + (case (lookup xi, Variable.def_sort ctxt xi) of (NONE, NONE) => Type.defaultS tsig | (NONE, SOME S) => S | (SOME S, NONE) => S @@ -629,6 +638,9 @@ " for type variable " ^ quote (Term.string_of_vname' xi))); in get end; +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 = @@ -647,7 +659,7 @@ in fun term_context ctxt = - {get_sort = get_sort ctxt (Variable.def_sort ctxt), + {get_sort = get_sort ctxt, map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), map_free = intern_skolem ctxt (Variable.def_type ctxt false)}; @@ -731,9 +743,8 @@ fun parse_typ ctxt text = let - val get_sort = get_sort ctxt (Variable.def_sort ctxt); val (syms, pos) = Syntax.parse_token Markup.typ text; - val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos) + val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos) handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos); in T end;