# HG changeset patch
# User wenzelm
# Date 1321012377 -3600
# Node ID 304437f4386946be8e2e11b9589da026bbf06598
# Parent  414732ebf89125a74b644ed7dd177636b68d6d8d
more scalable Proof_Context.prepare_sorts;
reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);

diff -r 414732ebf891 -r 304437f43869 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Nov 11 10:40:36 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Nov 11 12:52:57 2011 +0100
@@ -71,7 +71,7 @@
   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 prepare_sorts: Proof.context -> typ list -> typ 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
@@ -613,35 +613,47 @@
 
 (* sort constraints *)
 
-fun get_sort ctxt raw_text =
+fun prepare_sorts ctxt tys =
   let
     val tsig = tsig_of ctxt;
-
-    val text = distinct (op =) (map (apsnd (Type.minimize_sort tsig)) raw_text);
-    val _ =
-      (case duplicates (eq_fst (op =)) text of
-        [] => ()
-      | dups => error ("Inconsistent sort constraints for type variable(s) "
-          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
+    val defaultS = Type.defaultS tsig;
 
-    fun lookup xi =
-      (case AList.lookup (op =) text xi of
-        NONE => NONE
-      | SOME S => if S = dummyS then NONE else SOME S);
+    fun constraint (xi, S) env =
+      if S = dummyS then env
+      else
+        Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
+          handle Vartab.DUP _ =>
+            error ("Inconsistent sort constraints for type variable " ^
+              quote (Term.string_of_vname' xi));
+    val env =
+      (fold o fold_atyps)
+        (fn TFree (x, S) => constraint ((x, ~1), S)
+          | TVar v => constraint v
+          | _ => I) tys Vartab.empty;
 
-    fun get xi =
-      (case (lookup xi, Variable.def_sort ctxt xi) of
-        (NONE, NONE) => Type.defaultS tsig
+    fun get_sort xi =
+      (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
+        (NONE, NONE) => defaultS
       | (NONE, SOME S) => S
       | (SOME S, NONE) => S
       | (SOME S, SOME S') =>
           if Type.eq_sort tsig (S, S') then S'
-          else 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 get end;
+          else
+            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 check_tfree ctxt (x, S) = (x, get_sort ctxt [((x, ~1), S)] (x, ~1));
+fun check_tfree ctxt v = dest_TFree (singleton (prepare_sorts ctxt) (TFree v));
 
 
 (* certify terms *)
diff -r 414732ebf891 -r 304437f43869 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Nov 11 10:40:36 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Nov 11 12:52:57 2011 +0100
@@ -155,12 +155,8 @@
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
           if constrain_pos then
-            let val pos = Lexicon.pos_of_token tok in
-              if Position.is_reported pos then
-                [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
-                  Ast.Variable (Term_Position.encode pos)]]
-              else [ast_of pt]
-            end
+            [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
+              Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
           else [ast_of pt]
       | asts_of (Parser.Node (a, pts)) =
           let
@@ -798,37 +794,17 @@
 val apply_typ_uncheck = check fst true;
 val apply_term_uncheck = check snd true;
 
-fun prepare_sorts ctxt tys =
-  let
-    fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
-    val env =
-      (fold o fold_atyps)
-        (fn TFree (x, S) => constraint ((x, ~1), S)
-          | TVar v => constraint v
-          | _ => I) tys [];
-    val get_sort = Proof_Context.get_sort ctxt env;
-  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;
-
 in
 
 fun check_typs ctxt =
-  prepare_sorts ctxt #>
+  Proof_Context.prepare_sorts ctxt #>
   apply_typ_check ctxt #>
   Term_Sharing.typs (Proof_Context.theory_of ctxt);
 
 fun check_terms ctxt raw_ts =
   let
     val (ts, ps) = raw_ts
-      |> Term.burrow_types (prepare_sorts ctxt)
+      |> Term.burrow_types (Proof_Context.prepare_sorts ctxt)
       |> Type_Infer_Context.prepare_positions ctxt;
     val tys = map (Logic.mk_type o snd) ps;
     val (ts', tys') = ts @ tys