# HG changeset patch
# User wenzelm
# Date 1320868031 -3600
# Node ID fd58cbf8cae3bc75f95538a22a2e12a950a9552c
# Parent  aa35c9454a9569bc079ba03c3707a48667ebb913
tuned signature;
tuned;

diff -r aa35c9454a95 -r fd58cbf8cae3 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -224,7 +224,7 @@
   #> Code.abstype_interpretation ensure_term_of
   #> Code.datatype_interpretation ensure_term_of_code
   #> Code.abstype_interpretation ensure_abs_term_of_code
-  #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+  #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
   #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
 
 end;
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Isar/class.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -550,7 +550,7 @@
     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     |> Overloading.activate_improvable_syntax
-    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
+    |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
     |> Local_Theory.init NONE ""
        {define = Generic_Target.define foundation,
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -147,11 +147,11 @@
     val init_class_body =
       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
       #> Class.redeclare_operations thy sups
-      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
-      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
+      #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
+      #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
     val ((raw_supparams, _, raw_inferred_elems), _) =
       Proof_Context.init_global thy
-      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
+      |> Context.proof_map (Syntax_Phases.typ_check 5 "after_infer_fixate" (K after_infer_fixate))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
       | filter_element (e as Element.Fixes _) = SOME e
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -114,8 +114,8 @@
 
 val activate_improvable_syntax =
   Context.proof_map
-    (Syntax.context_term_check 0 "improvement" improve_term_check
-    #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
+    (Syntax_Phases.context_term_check 0 "improvement" improve_term_check
+    #> Syntax_Phases.context_term_uncheck 0 "improvement" improve_term_uncheck)
   #> set_primary_constraints;
 
 
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -83,6 +83,9 @@
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term
   val def_type: Proof.context -> indexname -> typ option
+  val standard_typ_check: Proof.context -> typ list -> typ list
+  val standard_term_check_finish: Proof.context -> term list -> term list
+  val standard_term_uncheck: Proof.context -> term list -> term list
   val goal_export: Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
@@ -666,23 +669,12 @@
   let val Mode {pattern, ...} = get_mode ctxt
   in Variable.def_type ctxt pattern end;
 
-local
-
 fun standard_typ_check ctxt =
-  map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
-  map (prepare_patternT ctxt);
-
-fun standard_term_uncheck ctxt =
-  map (contract_abbrevs ctxt);
+  map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt);
 
-in
+val standard_term_check_finish = prepare_patterns;
 
-val _ = Context.>>
- (Syntax.add_typ_check 0 "standard" standard_typ_check #>
-  Syntax.add_term_check 100 "fixate" prepare_patterns #>
-  Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
-
-end;
+fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt);
 
 
 
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -30,31 +30,6 @@
   val unparse_arity: Proof.context -> arity -> Pretty.T
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
-  val print_checks: Proof.context -> unit
-  val context_typ_check: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_check: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_typ_uncheck: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_uncheck: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
-    Context.generic -> Context.generic
-  val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
-    Context.generic -> Context.generic
-  val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
-    Context.generic -> Context.generic
-  val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
-    Context.generic -> Context.generic
-  val apply_typ_check: Proof.context -> typ list -> typ list
-  val apply_term_check: Proof.context -> term list -> term list
-  val apply_typ_uncheck: Proof.context -> typ list -> typ list
-  val apply_term_uncheck: Proof.context -> term list -> term list
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
@@ -244,88 +219,7 @@
 val unparse_term = operation #unparse_term;
 
 
-(* context-sensitive (un)checking *)
-
-type key = int * bool;
-
-structure Checks = Generic_Data
-(
-  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
-  type T =
-    ((key * ((string * typ check) * stamp) list) list *
-     (key * ((string * term check) * stamp) list) list);
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
-    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
-     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
-);
-
-fun print_checks ctxt =
-  let
-    fun split_checks checks =
-      List.partition (fn ((_, un), _) => not un) checks
-      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
-          #> sort (int_ord o pairself fst));
-    fun pretty_checks kind checks =
-      checks |> map (fn (i, names) => Pretty.block
-        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
-          Pretty.brk 1, Pretty.strs names]);
-
-    val (typs, terms) = Checks.get (Context.Proof ctxt);
-    val (typ_checks, typ_unchecks) = split_checks typs;
-    val (term_checks, term_unchecks) = split_checks terms;
-  in
-    pretty_checks "typ_checks" typ_checks @
-    pretty_checks "term_checks" term_checks @
-    pretty_checks "typ_unchecks" typ_unchecks @
-    pretty_checks "term_unchecks" term_unchecks
-  end |> Pretty.chunks |> Pretty.writeln;
-
-
-local
-
-fun context_check which (key: key) name f =
-  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
-
-fun simple_check eq f xs ctxt =
-  let val xs' = f ctxt xs
-  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
-
-in
-
-fun context_typ_check stage = context_check apfst (stage, false);
-fun context_term_check stage = context_check apsnd (stage, false);
-fun context_typ_uncheck stage = context_check apfst (stage, true);
-fun context_term_uncheck stage = context_check apsnd (stage, true);
-
-fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
-fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
-fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
-fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
-
-end;
-
-
-local
-
-fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
-fun check_all fs = perhaps_apply (map check_stage fs);
-
-fun check which uncheck ctxt0 xs0 =
-  let
-    val funs = which (Checks.get (Context.Proof ctxt0))
-      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
-      |> Library.sort (int_ord o pairself fst) |> map snd
-      |> not uncheck ? map rev;
-  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
-
-in
-
-val apply_typ_check = check fst false;
-val apply_term_check = check snd false;
-val apply_typ_uncheck = check fst true;
-val apply_term_uncheck = check snd true;
+(* (un)checking *)
 
 val check_typs = operation #check_typs;
 val check_terms = operation #check_terms;
@@ -338,8 +232,6 @@
 val uncheck_typs = operation #uncheck_typs;
 val uncheck_terms = operation #uncheck_terms;
 
-end;
-
 
 (* derived operations for algebra of sorts *)
 
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -13,6 +13,27 @@
     Position.report list * term Exn.result -> Position.report list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
+  val print_checks: Proof.context -> unit
+  val context_typ_check: int -> string ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val context_term_check: int -> string ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val context_typ_uncheck: int -> string ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val context_term_uncheck: int -> string ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
+    Context.generic -> Context.generic
+  val term_check: int -> string -> (Proof.context -> term list -> term list) ->
+    Context.generic -> Context.generic
+  val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
+    Context.generic -> Context.generic
+  val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
+    Context.generic -> Context.generic
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
@@ -692,6 +713,87 @@
 
 (** check/uncheck **)
 
+(* context-sensitive (un)checking *)
+
+type key = int * bool;
+
+structure Checks = Generic_Data
+(
+  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
+  type T =
+    ((key * ((string * typ check) * stamp) list) list *
+     (key * ((string * term check) * stamp) list) list);
+  val empty = ([], []);
+  val extend = I;
+  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
+    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
+     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
+);
+
+fun print_checks ctxt =
+  let
+    fun split_checks checks =
+      List.partition (fn ((_, un), _) => not un) checks
+      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
+          #> sort (int_ord o pairself fst));
+    fun pretty_checks kind checks =
+      checks |> map (fn (i, names) => Pretty.block
+        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
+          Pretty.brk 1, Pretty.strs names]);
+
+    val (typs, terms) = Checks.get (Context.Proof ctxt);
+    val (typ_checks, typ_unchecks) = split_checks typs;
+    val (term_checks, term_unchecks) = split_checks terms;
+  in
+    pretty_checks "typ_checks" typ_checks @
+    pretty_checks "term_checks" term_checks @
+    pretty_checks "typ_unchecks" typ_unchecks @
+    pretty_checks "term_unchecks" term_unchecks
+  end |> Pretty.chunks |> Pretty.writeln;
+
+
+local
+
+fun context_check which (key: key) name f =
+  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
+
+fun simple_check eq f xs ctxt =
+  let val xs' = f ctxt xs
+  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
+
+in
+
+fun context_typ_check stage = context_check apfst (stage, false);
+fun context_term_check stage = context_check apsnd (stage, false);
+fun context_typ_uncheck stage = context_check apfst (stage, true);
+fun context_term_uncheck stage = context_check apsnd (stage, true);
+
+fun typ_check key name f = context_typ_check key name (simple_check (op =) f);
+fun term_check key name f = context_term_check key name (simple_check (op aconv) f);
+fun typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
+fun term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
+
+end;
+
+
+local
+
+fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
+fun check_all fs = perhaps_apply (map check_stage fs);
+
+fun check which uncheck ctxt0 xs0 =
+  let
+    val funs = which (Checks.get (Context.Proof ctxt0))
+      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
+      |> Library.sort (int_ord o pairself fst) |> map snd
+      |> not uncheck ? map rev;
+  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
+
+val apply_typ_check = check fst false;
+val apply_term_check = check snd false;
+val apply_typ_uncheck = check fst true;
+val apply_term_uncheck = check snd true;
+
 fun prepare_types ctxt tys =
   let
     fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
@@ -708,20 +810,34 @@
         | T => T) tys
   end;
 
+in
+
 fun check_typs ctxt =
   prepare_types ctxt #>
-  Syntax.apply_typ_check ctxt #>
+  apply_typ_check ctxt #>
   Term_Sharing.typs (Proof_Context.theory_of ctxt);
 
 fun check_terms ctxt =
   Term.burrow_types (prepare_types ctxt) #>
-  Syntax.apply_term_check ctxt #>
+  apply_term_check ctxt #>
   Term_Sharing.terms (Proof_Context.theory_of ctxt);
 
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 
-val uncheck_typs = Syntax.apply_typ_uncheck;
-val uncheck_terms = Syntax.apply_term_uncheck;
+val uncheck_typs = apply_typ_uncheck;
+val uncheck_terms = apply_term_uncheck;
+
+end;
+
+
+(* standard phases *)
+
+val _ = Context.>>
+ (typ_check 0 "standard" Proof_Context.standard_typ_check #>
+  term_check 0 "standard"
+    (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
+  term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
+  term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
 
 
 
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/type_infer_context.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -259,9 +259,4 @@
     val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
   in ts' end;
 
-val _ =
-  Context.>>
-    (Syntax.add_term_check 0 "standard"
-      (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)));
-
 end;
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Tools/adhoc_overloading.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -132,8 +132,8 @@
 (* setup *)
 
 val setup = Context.theory_map
-  (Syntax.context_term_check 0 "adhoc_overloading" check
-   #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
-   #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck);
+  (Syntax_Phases.context_term_check 0 "adhoc_overloading" check
+   #> Syntax_Phases.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
+   #> Syntax_Phases.context_term_uncheck 0 "adhoc_overloading" uncheck);
 
 end;
diff -r aa35c9454a95 -r fd58cbf8cae3 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Tools/subtyping.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -806,7 +806,7 @@
 val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
 
 val add_term_check =
-  Syntax.add_term_check ~100 "coercions"
+  Syntax_Phases.term_check ~100 "coercions"
     (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);